--- a/src/Tools/IsaPlanner/isand.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Tools/IsaPlanner/isand.ML Fri Mar 06 15:58:56 2015 +0100
@@ -91,7 +91,7 @@
fun fix_alls_cterm ctxt i th =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm th);
+ val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
val (fixedbody, fvs) = fix_alls_term ctxt i (Thm.prop_of th);
val cfvs = rev (map cert fvs);
val ct_body = cert fixedbody;
@@ -140,7 +140,7 @@
*)
fun subgoal_thms th =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm th);
+ val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
val t = Thm.prop_of th;