equal
deleted
inserted
replaced
991 in |
991 in |
992 {name = name, locality = loc, kind = kind, combformula = combformula, |
992 {name = name, locality = loc, kind = kind, combformula = combformula, |
993 atomic_types = atomic_types} |
993 atomic_types = atomic_types} |
994 end |
994 end |
995 |
995 |
996 fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc presimp_consts |
996 fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc |
997 ((name, loc), t) = |
997 presimp_consts ((name, loc), t) = |
998 let val thy = Proof_Context.theory_of ctxt in |
998 let val thy = Proof_Context.theory_of ctxt in |
999 case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom |
999 case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom |
1000 |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name |
1000 |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name |
1001 loc Axiom of |
1001 loc Axiom of |
1002 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} => |
1002 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} => |