src/HOL/HOL.thy
 changeset 59621 291934bac95e parent 59586 ddf6deaadfe8 child 59628 2b15625b85fc
```     1.1 --- a/src/HOL/HOL.thy	Fri Mar 06 14:01:08 2015 +0100
1.2 +++ b/src/HOL/HOL.thy	Fri Mar 06 15:58:56 2015 +0100
1.3 @@ -1194,13 +1194,13 @@
1.4  let
1.5    val (f_Let_unfold, x_Let_unfold) =
1.6      let val [(_ \$ (f \$ x) \$ _)] = Thm.prems_of @{thm Let_unfold}
1.7 -    in (Thm.cterm_of @{theory} f, Thm.cterm_of @{theory} x) end
1.8 +    in (Thm.global_cterm_of @{theory} f, Thm.global_cterm_of @{theory} x) end
1.9    val (f_Let_folded, x_Let_folded) =
1.10      let val [(_ \$ (f \$ x) \$ _)] = Thm.prems_of @{thm Let_folded}
1.11 -    in (Thm.cterm_of @{theory} f, Thm.cterm_of @{theory} x) end;
1.12 +    in (Thm.global_cterm_of @{theory} f, Thm.global_cterm_of @{theory} x) end;
1.13    val g_Let_folded =
1.14      let val [(_ \$ _ \$ (g \$ _))] = Thm.prems_of @{thm Let_folded}
1.15 -    in Thm.cterm_of @{theory} g end;
1.16 +    in Thm.global_cterm_of @{theory} g end;
1.17    fun count_loose (Bound i) k = if i >= k then 1 else 0
1.18      | count_loose (s \$ t) k = count_loose s k + count_loose t k
1.19      | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
1.20 @@ -1222,9 +1222,9 @@
1.21        else
1.22          let
1.23            val n = case f of (Abs (x, _, _)) => x | _ => "x";
1.24 -          val cx = Thm.cterm_of thy x;
1.25 +          val cx = Thm.global_cterm_of thy x;
1.26            val xT = Thm.typ_of_cterm cx;
1.27 -          val cf = Thm.cterm_of thy f;
1.28 +          val cf = Thm.global_cterm_of thy f;
1.29            val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
1.30            val (_ \$ _ \$ g) = Thm.prop_of fx_g;
1.31            val g' = abstract_over (x,g);
1.32 @@ -1238,10 +1238,10 @@
1.33               else if (Envir.beta_eta_contract f) aconv (Envir.beta_eta_contract abs_g') then NONE (*avoid identity conversion*)
1.34               else let
1.35                     val g'x = abs_g'\$x;
1.36 -                   val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.cterm_of thy g'x));
1.37 +                   val g_g'x = Thm.symmetric (Thm.beta_conversion false (Thm.global_cterm_of thy g'x));
1.38                     val rl = cterm_instantiate
1.39 -                             [(f_Let_folded, Thm.cterm_of thy f), (x_Let_folded, cx),
1.40 -                              (g_Let_folded, Thm.cterm_of thy abs_g')]
1.41 +                             [(f_Let_folded, Thm.global_cterm_of thy f), (x_Let_folded, cx),
1.42 +                              (g_Let_folded, Thm.global_cterm_of thy abs_g')]
1.43                               @{thm Let_folded};
1.44                   in SOME (rl OF [Thm.transitive fx_g g_g'x])
1.45                   end)
```