# HG changeset patch
# User wenzelm
# Date 1425680081 -3600
# Node ID 2b15625b85fc331653d51f3f52e5df8a80c6eef5
# Parent  bb1e4a35d5064f118cf8074ab0fe69bf0f8a75f8
clarified context;
tuned;

diff -r bb1e4a35d506 -r 2b15625b85fc src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Mar 06 21:20:30 2015 +0100
+++ b/src/HOL/HOL.thy	Fri Mar 06 23:14:41 2015 +0100
@@ -1194,60 +1194,65 @@
 let
   val (f_Let_unfold, x_Let_unfold) =
     let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_unfold}
-    in (Thm.global_cterm_of @{theory} f, Thm.global_cterm_of @{theory} x) end
+    in apply2 (Thm.cterm_of @{context}) (f, x) end
   val (f_Let_folded, x_Let_folded) =
     let val [(_ $ (f $ x) $ _)] = Thm.prems_of @{thm Let_folded}
-    in (Thm.global_cterm_of @{theory} f, Thm.global_cterm_of @{theory} x) end;
+    in apply2 (Thm.cterm_of @{context}) (f, x) end;
   val g_Let_folded =
     let val [(_ $ _ $ (g $ _))] = Thm.prems_of @{thm Let_folded}
-    in Thm.global_cterm_of @{theory} g end;
+    in Thm.cterm_of @{context} 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)
     | count_loose _ _ = 0;
   fun is_trivial_let (Const (@{const_name Let}, _) $ x $ t) =
-   case t
-    of Abs (_, _, t') => count_loose t' 0 <= 1
-     | _ => true;
-in fn _ => fn ctxt => fn ct => if is_trivial_let (Thm.term_of ct)
-  then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
-  else let (*Norbert Schirmer's case*)
-    val thy = Proof_Context.theory_of ctxt;
-    val t = Thm.term_of ct;
-    val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
-  in Option.map (hd o Variable.export ctxt' ctxt o single)
-    (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
-      if is_Free x orelse is_Bound x orelse is_Const x
-      then SOME @{thm Let_def}
-      else
-        let
-          val n = case f of (Abs (x, _, _)) => x | _ => "x";
-          val cx = Thm.global_cterm_of thy x;
-          val xT = Thm.typ_of_cterm cx;
-          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);
-          val abs_g'= Abs (n,xT,g');
-        in (if (g aconv g')
-             then
-                let
-                  val rl =
-                    cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
-                in SOME (rl OF [fx_g]) end
-             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.global_cterm_of thy g'x));
-                   val rl = cterm_instantiate
-                             [(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)
-        end
-    | _ => NONE)
-  end
+    (case t of
+      Abs (_, _, t') => count_loose t' 0 <= 1
+    | _ => true);
+in
+  fn _ => fn ctxt => fn ct =>
+    if is_trivial_let (Thm.term_of ct)
+    then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
+    else
+      let (*Norbert Schirmer's case*)
+        val t = Thm.term_of ct;
+        val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
+      in
+        Option.map (hd o Variable.export ctxt' ctxt o single)
+          (case t' of Const (@{const_name Let},_) $ x $ f => (* x and f are already in normal form *)
+            if is_Free x orelse is_Bound x orelse is_Const x
+            then SOME @{thm Let_def}
+            else
+              let
+                val n = case f of (Abs (x, _, _)) => x | _ => "x";
+                val cx = Thm.cterm_of ctxt x;
+                val xT = Thm.typ_of_cterm cx;
+                val cf = Thm.cterm_of ctxt f;
+                val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
+                val (_ $ _ $ g) = Thm.prop_of fx_g;
+                val g' = abstract_over (x, g);
+                val abs_g'= Abs (n, xT, g');
+              in
+                if g aconv g' then
+                  let
+                    val rl =
+                      cterm_instantiate [(f_Let_unfold, cf), (x_Let_unfold, cx)] @{thm Let_unfold};
+                  in SOME (rl OF [fx_g]) end
+                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 ctxt g'x));
+                    val rl =
+                      @{thm Let_folded} |> cterm_instantiate
+                        [(f_Let_folded, Thm.cterm_of ctxt f),
+                         (x_Let_folded, cx),
+                         (g_Let_folded, Thm.cterm_of ctxt abs_g')];
+                  in SOME (rl OF [Thm.transitive fx_g g_g'x]) end
+              end
+          | _ => NONE)
+      end
 end *}
 
 lemma True_implies_equals: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"