diff -r a2d056424d3c -r 929984c529d3 src/Tools/eqsubst.ML
--- a/src/Tools/eqsubst.ML	Fri Mar 06 23:55:55 2015 +0100
+++ b/src/Tools/eqsubst.ML	Fri Mar 06 23:56:43 2015 +0100
@@ -259,14 +259,11 @@
     val th = Thm.incr_indexes 1 gth;
     val tgt_term = Thm.prop_of th;
 
-    val thy = Thm.theory_of_thm th;
-    val cert = Thm.global_cterm_of thy;
-
     val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
-    val cfvs = rev (map cert fvs);
+    val cfvs = rev (map (Thm.cterm_of ctxt) fvs);
 
     val conclterm = Logic.strip_imp_concl fixedbody;
-    val conclthm = Thm.trivial (cert conclterm);
+    val conclthm = Thm.trivial (Thm.cterm_of ctxt conclterm);
     val maxidx = Thm.maxidx_of th;
     val ft =
       (Zipper.move_down_right (* ==> *)
@@ -274,7 +271,7 @@
        o Zipper.mktop
        o Thm.prop_of) conclthm
   in
-    ((cfvs, conclthm), (thy, maxidx, ft))
+    ((cfvs, conclthm), (Proof_Context.theory_of ctxt, maxidx, ft))
   end;
 
 (* substitute using an object or meta level equality *)