equal
deleted
inserted
replaced
54 val new_skolemizer = |
54 val new_skolemizer = |
55 Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) |
55 Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) |
56 |
56 |
57 (* Designed to work also with monomorphic instances of polymorphic theorems. *) |
57 (* Designed to work also with monomorphic instances of polymorphic theorems. *) |
58 fun have_common_thm ths1 ths2 = |
58 fun have_common_thm ths1 ths2 = |
59 exists (member (untyped_aconv o pairself prop_of) ths1) |
59 exists (member (metis_aconv_untyped o pairself prop_of) ths1) |
60 (map Meson.make_meta_clause ths2) |
60 (map Meson.make_meta_clause ths2) |
61 |
61 |
62 (*Determining which axiom clauses are actually used*) |
62 (*Determining which axiom clauses are actually used*) |
63 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
63 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
64 | used_axioms _ _ = NONE |
64 | used_axioms _ _ = NONE |