--- a/src/Tools/eqsubst.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Tools/eqsubst.ML Fri Mar 06 15:58:56 2015 +0100
@@ -260,7 +260,7 @@
val tgt_term = Thm.prop_of th;
val thy = Thm.theory_of_thm th;
- val cert = Thm.cterm_of thy;
+ val cert = Thm.global_cterm_of thy;
val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
val cfvs = rev (map cert fvs);
@@ -349,7 +349,7 @@
val tgt_term = Thm.prop_of th;
val thy = Thm.theory_of_thm th;
- val cert = Thm.cterm_of thy;
+ val cert = Thm.global_cterm_of thy;
val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
val cfvs = rev (map cert fvs);