equal
deleted
inserted
replaced
58 |
58 |
59 fun transfer_thm_of ctxt ths t = |
59 fun transfer_thm_of ctxt ths t = |
60 let |
60 let |
61 val thy = ProofContext.theory_of ctxt; |
61 val thy = ProofContext.theory_of ctxt; |
62 val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt) |
62 val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt) |
63 val meta = LocalDefs.meta_rewrite_rule (Context.Proof ctxt) |
63 val meta = LocalDefs.meta_rewrite_rule ctxt |
64 val unfolds' = map meta unfolds and refolds' = map meta refolds; |
64 val unfolds' = map meta unfolds and refolds' = map meta refolds; |
65 val (_$_$t') = concl_of (Tactic.rewrite true unfolds' (cterm_of thy t)) |
65 val (_$_$t') = concl_of (Tactic.rewrite true unfolds' (cterm_of thy t)) |
66 val u = unstar_term consts t' |
66 val u = unstar_term consts t' |
67 val tac = |
67 val tac = |
68 rewrite_goals_tac (ths @ refolds' @ unfolds') THEN |
68 rewrite_goals_tac (ths @ refolds' @ unfolds') THEN |