src/Tools/IsaPlanner/rw_inst.ML
changeset 59621 291934bac95e
parent 58318 f95754ca7082
child 59641 a2d056424d3c
     1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  *)
     1.5  fun allify_conditions Ts th =
     1.6    let
     1.7 -    val cert = Thm.cterm_of (Thm.theory_of_thm th);
     1.8 +    val cert = Thm.global_cterm_of (Thm.theory_of_thm th);
     1.9  
    1.10      fun allify (x, T) t =
    1.11        Logic.all_const T $ Abs (x, T, Term.abstract_over (Free (x, T), t));
    1.12 @@ -62,7 +62,7 @@
    1.13  (* Note, we take abstraction in the order of last abstraction first *)
    1.14  fun mk_abstractedrule ctxt TsFake Ts rule =
    1.15    let
    1.16 -    val cert = Thm.cterm_of (Thm.theory_of_thm rule);
    1.17 +    val cert = Thm.global_cterm_of (Thm.theory_of_thm rule);
    1.18  
    1.19      (* now we change the names of temporary free vars that represent
    1.20         bound vars with binders outside the redex *)
    1.21 @@ -172,8 +172,8 @@
    1.22  fun rw ctxt ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
    1.23    let
    1.24      val thy = Thm.theory_of_thm target_thm;
    1.25 -    val cert = Thm.cterm_of thy;
    1.26 -    val certT = Thm.ctyp_of thy;
    1.27 +    val cert = Thm.global_cterm_of thy;
    1.28 +    val certT = Thm.global_ctyp_of thy;
    1.29  
    1.30      (* fix all non-instantiated tvars *)
    1.31      val (fixtyinsts, othertfrees) = (* FIXME proper context!? *)