# HG changeset patch
# User wenzelm
# Date 1257191448 -3600
# Node ID d64545e6cba59a57fc46e6c9fd5633ea109175ce
# Parent  acea2f336721977eb60cea7ee625bd56eca2f4c9
modernized structure Proof_Syntax;

diff -r acea2f336721 -r d64545e6cba5 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 02 20:48:08 2009 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 02 20:50:48 2009 +0100
@@ -15,8 +15,8 @@
 
 open Proofterm;
 
-val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
-    Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
+val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
+    Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT)
 
   (** eliminate meta-equality rules **)
 
diff -r acea2f336721 -r d64545e6cba5 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 20:48:08 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 20:50:48 2009 +0100
@@ -460,11 +460,11 @@
           val prop = Thm.full_prop_of thm;
           val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
         in
-          ProofSyntax.pretty_proof ctxt
+          Proof_Syntax.pretty_proof ctxt
             (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
         end
     | SOME args => Pretty.chunks
-        (map (ProofSyntax.pretty_proof_of (Proof.context_of state) full)
+        (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
           (Proof.get_thmss state args)));
 
 fun string_of_prop state s =
diff -r acea2f336721 -r d64545e6cba5 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Mon Nov 02 20:48:08 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Mon Nov 02 20:50:48 2009 +0100
@@ -300,7 +300,7 @@
     val rtypes = map fst types;
     val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
     val thy' = add_syntax thy;
-    val rd = ProofSyntax.read_proof thy' false
+    val rd = Proof_Syntax.read_proof thy' false;
   in fn (thm, (vs, s1, s2)) =>
     let
       val name = Thm.get_name thm;
diff -r acea2f336721 -r d64545e6cba5 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Mon Nov 02 20:48:08 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Mon Nov 02 20:50:48 2009 +0100
@@ -19,7 +19,7 @@
   val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
 end;
 
-structure ProofSyntax : PROOF_SYNTAX =
+structure Proof_Syntax : PROOF_SYNTAX =
 struct
 
 open Proofterm;
diff -r acea2f336721 -r d64545e6cba5 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Nov 02 20:48:08 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Nov 02 20:50:48 2009 +0100
@@ -478,7 +478,7 @@
     val ctxt' = Variable.auto_fixes eq ctxt;
   in ProofContext.pretty_term_abbrev ctxt' eq end;
 
-fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
+fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 
 fun pretty_theory ctxt name =
   (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);