fix

HOL-Theorem-Prover · Nov 11, 2024 · 8b59927 · 8b59927
1 parent c15d5e5
commit 8b59927
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)))
+  fst(snd(Lib.first (fn (_,(th,_,_)) => eq (h,c) th) (DB.match [] c)))
 handle HOL_ERR _ =>
   from_net ths (h,c)
 handle HOL_ERR e => let