modernized structure Proof_Syntax;
authorwenzelm
Mon Nov 02 20:50:48 2009 +0100 (2009-11-02)
changeset 33388d64545e6cba5
parent 33387 acea2f336721
child 33389 bb3a5fa94a91
modernized structure Proof_Syntax;
src/HOL/Tools/rewrite_hol_proof.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 02 20:48:08 2009 +0100
     1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 02 20:50:48 2009 +0100
     1.3 @@ -15,8 +15,8 @@
     1.4  
     1.5  open Proofterm;
     1.6  
     1.7 -val rews = map (pairself (ProofSyntax.proof_of_term @{theory} true) o
     1.8 -    Logic.dest_equals o Logic.varify o ProofSyntax.read_term @{theory} propT)
     1.9 +val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
    1.10 +    Logic.dest_equals o Logic.varify o Proof_Syntax.read_term @{theory} propT)
    1.11  
    1.12    (** eliminate meta-equality rules **)
    1.13  
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 20:48:08 2009 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Nov 02 20:50:48 2009 +0100
     2.3 @@ -460,11 +460,11 @@
     2.4            val prop = Thm.full_prop_of thm;
     2.5            val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
     2.6          in
     2.7 -          ProofSyntax.pretty_proof ctxt
     2.8 +          Proof_Syntax.pretty_proof ctxt
     2.9              (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
    2.10          end
    2.11      | SOME args => Pretty.chunks
    2.12 -        (map (ProofSyntax.pretty_proof_of (Proof.context_of state) full)
    2.13 +        (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
    2.14            (Proof.get_thmss state args)));
    2.15  
    2.16  fun string_of_prop state s =
     3.1 --- a/src/Pure/Proof/extraction.ML	Mon Nov 02 20:48:08 2009 +0100
     3.2 +++ b/src/Pure/Proof/extraction.ML	Mon Nov 02 20:50:48 2009 +0100
     3.3 @@ -300,7 +300,7 @@
     3.4      val rtypes = map fst types;
     3.5      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
     3.6      val thy' = add_syntax thy;
     3.7 -    val rd = ProofSyntax.read_proof thy' false
     3.8 +    val rd = Proof_Syntax.read_proof thy' false;
     3.9    in fn (thm, (vs, s1, s2)) =>
    3.10      let
    3.11        val name = Thm.get_name thm;
     4.1 --- a/src/Pure/Proof/proof_syntax.ML	Mon Nov 02 20:48:08 2009 +0100
     4.2 +++ b/src/Pure/Proof/proof_syntax.ML	Mon Nov 02 20:50:48 2009 +0100
     4.3 @@ -19,7 +19,7 @@
     4.4    val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
     4.5  end;
     4.6  
     4.7 -structure ProofSyntax : PROOF_SYNTAX =
     4.8 +structure Proof_Syntax : PROOF_SYNTAX =
     4.9  struct
    4.10  
    4.11  open Proofterm;
     5.1 --- a/src/Pure/Thy/thy_output.ML	Mon Nov 02 20:48:08 2009 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Nov 02 20:50:48 2009 +0100
     5.3 @@ -478,7 +478,7 @@
     5.4      val ctxt' = Variable.auto_fixes eq ctxt;
     5.5    in ProofContext.pretty_term_abbrev ctxt' eq end;
     5.6  
     5.7 -fun pretty_prf full ctxt = ProofSyntax.pretty_proof_of ctxt full;
     5.8 +fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
     5.9  
    5.10  fun pretty_theory ctxt name =
    5.11    (Theory.requires (ProofContext.theory_of ctxt) name "presentation"; Pretty.str name);