Fix OpenTheoryReader's compile errors in light of located_thms

HOL-Theorem-Prover · Nov 12, 2024 · a05c02a · a05c02a
1 parent 6f94f13
commit a05c02a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/opentheory/reader/OpenTheoryReader.sml b/src/opentheory/reader/OpenTheoryReader.sml
@@ -122,7 +122,7 @@ in
 fun axiom_in_db ths (h,c) =
     from_net base_thms (h,c)
 handle HOL_ERR _ =>
-  fst(snd(Lib.first (fn (_,(th,_)) => eq (h,c) th) (DB.match [] c)))
+  #1(#2(Lib.first (fn (_,(th,_,_)) => eq (h,c) th) (DB.match [] c)))
 handle HOL_ERR _ =>
   from_net ths (h,c)
 handle HOL_ERR e => let