--- a/src/Tools/IsaPlanner/rw_inst.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML Fri Mar 06 15:58:56 2015 +0100
@@ -32,7 +32,7 @@
*)
fun allify_conditions Ts th =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm th);
+ val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
fun allify (x, T) t =
Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
@@ -62,7 +62,7 @@
(* Note, we take abstraction in the order of last abstraction first *)
fun mk_abstractedrule ctxt TsFake Ts rule =
let
- val cert = Thm.cterm_of (Thm.theory_of_thm rule);
+ val cert = Thm.global_cterm_of (Thm.theory_of_thm rule);
(* now we change the names of temporary free vars that represent
bound vars with binders outside the redex *)
@@ -172,8 +172,8 @@
fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
let
val thy = Thm.theory_of_thm target_thm;
- val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
+ val cert = Thm.global_cterm_of thy;
+ val certT = Thm.global_ctyp_of thy;
(* fix all non-instantiated tvars *)
val (fixtyinsts, othertfrees) = (* FIXME proper context!? *)