--- a/src/Pure/Tools/rule_insts.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Fri Mar 06 15:58:56 2015 +0100
@@ -116,8 +116,8 @@
val inst_tvars = map_filter (make_instT (instT2 o instT1)) tvars;
val inst_vars = map_filter (make_inst inst2) vars2;
in
- (map (apply2 (Thm.ctyp_of thy)) inst_tvars,
- map (apply2 (Thm.cterm_of thy)) inst_vars)
+ (map (apply2 (Thm.global_ctyp_of thy)) inst_tvars,
+ map (apply2 (Thm.global_cterm_of thy)) inst_vars)
end;
fun where_rule ctxt mixed_insts fixes thm =
@@ -250,7 +250,7 @@
val cenv =
map
(fn (xi, t) =>
- apply2 (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
+ apply2 (Thm.global_cterm_of thy) (Var (xi, fastype_of t), t))
(distinct
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
(xis ~~ ts));
@@ -264,7 +264,7 @@
fun liftterm t =
fold_rev absfree (param_names ~~ paramTs) (Logic.incr_indexes (paramTs, inc) t);
fun liftpair (cv, ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct);
- val lifttvar = apply2 (Thm.ctyp_of thy o Logic.incr_tvar inc);
+ val lifttvar = apply2 (Thm.global_ctyp_of thy o Logic.incr_tvar inc);
val rule = Drule.instantiate_normalize
(map lifttvar envT', map liftpair cenv)
(Thm.lift_rule cgoal thm)
@@ -283,7 +283,7 @@
let
val thy = Thm.theory_of_thm rl;
val maxidx = Thm.maxidx_of rl;
- fun cvar xi = Thm.cterm_of thy (Var (xi, propT));
+ fun cvar xi = Thm.global_cterm_of thy (Var (xi, propT));
val revcut_rl' =
Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
(cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;