--- a/src/HOL/Hyperreal/transfer.ML Fri Apr 20 11:21:36 2007 +0200
+++ b/src/HOL/Hyperreal/transfer.ML Fri Apr 20 11:21:37 2007 +0200
@@ -59,13 +59,14 @@
fun transfer_thm_of ctxt ths t =
let
val thy = ProofContext.theory_of ctxt;
- val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt)
- val meta = LocalDefs.meta_rewrite_rule ctxt
+ val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
+ val meta = LocalDefs.meta_rewrite_rule ctxt;
+ val ths' = map meta ths;
val unfolds' = map meta unfolds and refolds' = map meta refolds;
val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
val u = unstar_term consts t'
val tac =
- rewrite_goals_tac (ths @ refolds' @ unfolds') THEN
+ rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
ALLGOALS ObjectLogic.full_atomize_tac THEN
match_tac [transitive_thm] 1 THEN
resolve_tac [transfer_start] 1 THEN