# HG changeset patch
# User wenzelm
# Date 1312814339 -7200
# Node ID fda143b5c2f559385b485dd7290f5489fc4f0215
# Parent  be825a69fc67037ae153975284aad2269fba0f04
modernized strcture Proof_Checker;

diff -r be825a69fc67 -r fda143b5c2f5 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Aug 08 16:09:34 2011 +0200
+++ b/src/Pure/Proof/extraction.ML	Mon Aug 08 16:38:59 2011 +0200
@@ -795,7 +795,7 @@
              |> Global_Theory.store_thm (Binding.qualified_name (corr_name s vs),
                   Thm.varifyT_global (funpow (length (vars_of corr_prop))
                     (Thm.forall_elim_var 0) (Thm.forall_intr_frees
-                      (ProofChecker.thm_of_proof thy'
+                      (Proof_Checker.thm_of_proof thy'
                        (fst (Proofterm.freeze_thaw_prf prf))))))
              |> snd
              |> fold Code.add_default_eqn def_thms
diff -r be825a69fc67 -r fda143b5c2f5 src/Pure/Proof/proofchecker.ML
--- a/src/Pure/Proof/proofchecker.ML	Mon Aug 08 16:09:34 2011 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Mon Aug 08 16:38:59 2011 +0200
@@ -10,17 +10,17 @@
   val thm_of_proof : theory -> Proofterm.proof -> thm
 end;
 
-structure ProofChecker : PROOF_CHECKER =
+structure Proof_Checker : PROOF_CHECKER =
 struct
 
 (***** construct a theorem out of a proof term *****)
 
 fun lookup_thm thy =
-  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty
-  in
-    (fn s => case Symtab.lookup tab s of
-       NONE => error ("Unknown theorem " ^ quote s)
-     | SOME thm => thm)
+  let val tab = fold_rev Symtab.update (Global_Theory.all_thms_of thy) Symtab.empty in
+    fn s =>
+      (case Symtab.lookup tab s of
+        NONE => error ("Unknown theorem " ^ quote s)
+      | SOME thm => thm)
   end;
 
 val beta_eta_convert =
@@ -87,10 +87,12 @@
           let
             val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
             val {prop, ...} = rep_thm 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');
+            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)) =