--- a/src/HOL/NSA/transfer.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/NSA/transfer.ML Fri Mar 06 15:58:56 2015 +0100
@@ -57,7 +57,7 @@
val meta = Local_Defs.meta_rewrite_rule ctxt;
val ths' = map meta ths;
val unfolds' = map meta unfolds and refolds' = map meta refolds;
- val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of thy t))
+ val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.global_cterm_of thy t))
val u = unstar_term consts t'
val tac =
rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN