# HG changeset patch
# User wenzelm
# Date 1312829232 -7200
# Node ID 9f17ede679e9eaafe46d8bd8ee41caea0c48a45b
# Parent  656ff92bad48615b2e7d04ee91d9feccfcd98bae
tuned thm_of_proof: build lookup table within closure;

diff -r 656ff92bad48 -r 9f17ede679e9 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Mon Aug 08 20:21:49 2011 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Mon Aug 08 20:47:12 2011 +0200
@@ -68,76 +68,78 @@
        ""])
   end;
 
-fun thm_of_proof thy prf =
-  let
-    val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
-    val lookup = lookup_thm thy;
-
-    fun thm_of_atom thm Ts =
+fun thm_of_proof thy =
+  let val lookup = lookup_thm thy in
+    fn prf =>
       let
-        val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
-        val (fmap, thm') = Thm.varifyT_global' [] thm;
-        val ctye = map (pairself (Thm.ctyp_of thy))
-          (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
-      in
-        Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
-      end;
+        val prf_names = Proofterm.fold_proof_terms Term.declare_term_frees (K I) prf Name.context;
 
-    fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
-          let
-            val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
-            val prop = Thm.prop_of thm;
-            val _ =
-              if is_equal prop prop' then ()
-              else
-                error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
-                  Syntax.string_of_term_global thy prop ^ "\n\n" ^
-                  Syntax.string_of_term_global thy prop');
-          in thm_of_atom thm Ts end
-
-      | thm_of _ _ (PAxm (name, _, SOME Ts)) =
-          thm_of_atom (Thm.axiom thy name) Ts
-
-      | thm_of _ Hs (PBound i) = nth Hs i
-
-      | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
+        fun thm_of_atom thm Ts =
           let
-            val (x, names') = Name.variant s names;
-            val thm = thm_of ((x, T) :: vs, names') Hs prf
+            val tvars = Term.add_tvars (Thm.full_prop_of thm) [] |> rev;
+            val (fmap, thm') = Thm.varifyT_global' [] thm;
+            val ctye = map (pairself (Thm.ctyp_of thy))
+              (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
           in
-            Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
-          end
+            Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
+          end;
 
-      | thm_of (vs, names) Hs (prf % SOME t) =
-          let
-            val thm = thm_of (vs, names) Hs prf;
-            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
-          in
-            Thm.forall_elim ct thm
-            handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
-          end
+        fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
+              let
+                val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
+                val prop = Thm.prop_of thm;
+                val _ =
+                  if is_equal prop prop' then ()
+                  else
+                    error ("Duplicate use of theorem name " ^ quote name ^ "\n" ^
+                      Syntax.string_of_term_global thy prop ^ "\n\n" ^
+                      Syntax.string_of_term_global thy prop');
+              in thm_of_atom thm Ts end
+
+          | thm_of _ _ (PAxm (name, _, SOME Ts)) =
+              thm_of_atom (Thm.axiom thy name) Ts
+
+          | thm_of _ Hs (PBound i) = nth Hs i
+
+          | thm_of (vs, names) Hs (Abst (s, SOME T, prf)) =
+              let
+                val (x, names') = Name.variant s names;
+                val thm = thm_of ((x, T) :: vs, names') Hs prf
+              in
+                Thm.forall_intr (Thm.cterm_of thy (Free (x, T))) thm
+              end
 
-      | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
-          let
-            val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
-            val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
-          in
-            Thm.implies_intr ct thm
-          end
+          | thm_of (vs, names) Hs (prf % SOME t) =
+              let
+                val thm = thm_of (vs, names) Hs prf;
+                val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+              in
+                Thm.forall_elim ct thm
+                handle THM (s, _, _) => appl_error thy pretty_term vs Hs s prf t
+              end
 
-      | thm_of vars Hs (prf %% prf') =
-          let
-            val thm = beta_eta_convert (thm_of vars Hs prf);
-            val thm' = beta_eta_convert (thm_of vars Hs prf');
-          in
-            Thm.implies_elim thm thm'
-            handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
-          end
+          | thm_of (vs, names) Hs (AbsP (s, SOME t, prf)) =
+              let
+                val ct = Thm.cterm_of thy (Term.subst_bounds (map Free vs, t));
+                val thm = thm_of (vs, names) (Thm.assume ct :: Hs) prf;
+              in
+                Thm.implies_intr ct thm
+              end
 
-      | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
+          | thm_of vars Hs (prf %% prf') =
+              let
+                val thm = beta_eta_convert (thm_of vars Hs prf);
+                val thm' = beta_eta_convert (thm_of vars Hs prf');
+              in
+                Thm.implies_elim thm thm'
+                handle THM (s, _, _) => appl_error thy pretty_prf (fst vars) Hs s prf prf'
+              end
 
-      | thm_of _ _ _ = error "thm_of_proof: partial proof term";
+          | thm_of _ _ (Hyp t) = Thm.assume (Thm.cterm_of thy t)
 
-  in beta_eta_convert (thm_of ([], prf_names) [] prf) end;
+          | thm_of _ _ _ = error "thm_of_proof: partial proof term";
+
+      in beta_eta_convert (thm_of ([], prf_names) [] prf) end
+  end;
 
 end;