equal
deleted
inserted
replaced
457 ProofContext.add_fixes_i fixed |> snd |> |
457 ProofContext.add_fixes_i fixed |> snd |> |
458 (fold o fold) Variable.auto_fixes propss; |
458 (fold o fold) Variable.auto_fixes propss; |
459 |
459 |
460 val export = Variable.export_morphism goal_ctxt context; |
460 val export = Variable.export_morphism goal_ctxt context; |
461 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
461 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
462 val exp_term = Drule.term_rule thy (singleton exp_fact); |
462 val exp_term = TermSubst.zero_var_indexes o Morphism.term export; |
463 val exp_typ = Logic.type_map exp_term; |
463 val exp_typ = Logic.type_map exp_term; |
464 val export' = |
464 val export' = |
465 Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
465 Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; |
466 in ((propss, deps, export'), goal_ctxt) end; |
466 in ((propss, deps, export'), goal_ctxt) end; |
467 |
467 |
686 |> apfst (curry Notes Thm.assumptionK) |
686 |> apfst (curry Notes Thm.assumptionK) |
687 | assumes_to_notes e axms = (e, axms); |
687 | assumes_to_notes e axms = (e, axms); |
688 |
688 |
689 fun defines_to_notes thy (Defines defs) = |
689 fun defines_to_notes thy (Defines defs) = |
690 Notes (Thm.definitionK, map (fn (a, (def, _)) => |
690 Notes (Thm.definitionK, map (fn (a, (def, _)) => |
691 (a, [([Assumption.assume (cterm_of thy def)], [])])) defs) |
691 (a, [([Assumption.assume (cterm_of thy def)], |
|
692 [(Attrib.internal o K) NewLocale.witness_attrib])])) defs) |
692 | defines_to_notes _ e = e; |
693 | defines_to_notes _ e = e; |
693 |
694 |
694 fun gen_add_locale prep_decl |
695 fun gen_add_locale prep_decl |
695 bname predicate_name raw_imprt raw_body thy = |
696 bname predicate_name raw_imprt raw_body thy = |
696 let |
697 let |