modernized strcture Proof_Checker;

--- 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

--- 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)) =