equal
deleted
inserted
replaced
547 |
547 |
548 val goal_ctxt = ctxt |
548 val goal_ctxt = ctxt |
549 |> fix_params fixed |
549 |> fix_params fixed |
550 |> (fold o fold) Proof_Context.augment (propss @ eq_propss); |
550 |> (fold o fold) Proof_Context.augment (propss @ eq_propss); |
551 |
551 |
552 val export = Variable.export_morphism goal_ctxt ctxt; |
552 val export = Proof_Context.export_morphism goal_ctxt ctxt; |
553 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
553 val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; |
554 val exp_term = Term_Subst.zero_var_indexes o Morphism.term export; |
554 val exp_term = Term_Subst.zero_var_indexes o Morphism.term export; |
555 val exp_typ = Logic.type_map exp_term; |
555 val exp_typ = Logic.type_map exp_term; |
556 val export' = |
556 val export' = |
557 Morphism.morphism "Expression.prep_goal" |
557 Morphism.morphism "Expression.prep_goal" |