--- a/src/HOL/HOL.thy Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/HOL.thy Fri Mar 06 15:58:56 2015 +0100
@@ -1194,13 +1194,13 @@
let
val (f_Let_unfold, x_Let_unfold) =
let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
- in (Thm.cterm_of @{theory} f, Thm.cterm_of @{theory} x) end
+ in (Thm.global_cterm_of @{theory} f, Thm.global_cterm_of @{theory} x) end
val (f_Let_folded, x_Let_folded) =
let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded}
- in (Thm.cterm_of @{theory} f, Thm.cterm_of @{theory} x) end;
+ in (Thm.global_cterm_of @{theory} f, Thm.global_cterm_of @{theory} x) end;
val g_Let_folded =
let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded}
- in Thm.cterm_of @{theory} g end;
+ in Thm.global_cterm_of @{theory} g end;
fun count_loose (Bound i) k = if i >= k then 1 else 0
| count_loose (s $ t) k = count_loose s k + count_loose t k
| count_loose (Abs (_, _, t)) k = count_loose t (k + 1)
@@ -1222,9 +1222,9 @@
else
let
val n = case f of (Abs (x, _, _)) => x | _ => "x";
- val cx = Thm.cterm_of thy x;
+ val cx = Thm.global_cterm_of thy x;
val xT = Thm.typ_of_cterm cx;
- val cf = Thm.cterm_of thy f;
+ val cf = Thm.global_cterm_of thy f;
val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
val (_ $ _ $ g) = Thm.prop_of fx_g;
val g' = abstract_over (x,g);
@@ -1238,10 +1238,10 @@
else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*)
else let
val g'x = abs_g'$x;
- val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of thy g'x));
+ val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.global_cterm_of thy g'x));
val rl = cterm_instantiate
- [(f_Let_folded, Thm.cterm_of thy f), (x_Let_folded, cx),
- (g_Let_folded, Thm.cterm_of thy abs_g')]
+ [(f_Let_folded, Thm.global_cterm_of thy f), (x_Let_folded, cx),
+ (g_Let_folded, Thm.global_cterm_of thy abs_g')]
@{thm Let_folded};
in SOME (rl OF [Thm.transitive fx_g g_g'x])
end)