# HG changeset patch
# User wenzelm
# Date 1572618203 -3600
# Node ID 9dab828cbbc1282759d17e3bfc016eeab7e20a70
# Parent  7abe5abb4c050da3a66f6cd80a56df6802a332e2
clarified modules (again);

diff -r 7abe5abb4c05 -r 9dab828cbbc1 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Nov 01 15:09:55 2019 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Nov 01 15:23:23 2019 +0100
@@ -7,6 +7,7 @@
 signature PROOF_SYNTAX =
 sig
   val add_proof_syntax: theory -> theory
+  val term_of_proof: proof -> term
   val proof_of_term: theory -> bool -> term -> Proofterm.proof
   val read_term: theory -> bool -> typ -> string -> term
   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
@@ -22,7 +23,7 @@
 
 (**** add special syntax for embedding proof terms ****)
 
-val proofT = Proofterm.proofT;
+val proofT = Type ("Pure.proof", []);
 
 local
 
@@ -80,7 +81,60 @@
   |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
 
 
-(**** translation between proof terms and pure terms ****)
+
+(** proof terms as pure terms **)
+
+(* term_of_proof *)
+
+local
+
+val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT);
+val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT);
+val Hypt = Const ("Pure.Hyp", propT --> proofT);
+val Oraclet = Const ("Pure.Oracle", propT --> proofT);
+val MinProoft = Const ("Pure.MinProof", proofT);
+
+fun AppT T prf =
+  Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T;
+
+fun OfClasst (T, c) =
+  let val U = Term.itselfT T --> propT
+  in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
+
+fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
+      fold AppT (these Ts)
+        (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
+  | term_of _ (PAxm (name, _, Ts)) =
+      fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
+  | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
+  | term_of _ (PBound i) = Bound i
+  | term_of Ts (Abst (s, opT, prf)) =
+      let val T = the_default dummyT opT in
+        Const ("Pure.Abst", (T --> proofT) --> proofT) $
+          Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
+      end
+  | term_of Ts (AbsP (s, t, prf)) =
+      AbsPt $ the_default Term.dummy_prop t $
+        Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
+  | term_of Ts (prf1 %% prf2) =
+      AppPt $ term_of Ts prf1 $ term_of Ts prf2
+  | term_of Ts (prf % opt) =
+      let
+        val t = the_default Term.dummy opt;
+        val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
+      in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
+  | term_of _ (Hyp t) = Hypt $ t
+  | term_of _ (Oracle (_, t, _)) = Oraclet $ t
+  | term_of _ MinProof = MinProoft;
+
+in
+
+val term_of_proof = term_of [];
+
+end;
+
+
+(* proof_of_term *)
 
 fun proof_of_term thy ty =
   let
@@ -194,7 +248,7 @@
 fun pretty_proof ctxt prf =
   Proof_Context.pretty_term_abbrev
     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
-    (Proofterm.term_of_proof prf);
+    (term_of_proof prf);
 
 fun pretty_standard_proof_of ctxt full thm =
   pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
diff -r 7abe5abb4c05 -r 9dab828cbbc1 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Nov 01 15:09:55 2019 +0100
+++ b/src/Pure/proofterm.ML	Fri Nov 01 15:23:23 2019 +0100
@@ -103,8 +103,6 @@
   val prf_subst_bounds: term list -> proof -> proof
   val prf_subst_pbounds: proof list -> proof -> proof
   val freeze_thaw_prf: proof -> proof * (proof -> proof)
-  val proofT: typ
-  val term_of_proof: proof -> term
 
   (*proof terms for specific inference rules*)
   val trivial_proof: proof
@@ -835,59 +833,6 @@
 
 
 
-(** proof terms as pure terms **)
-
-val proofT = Type ("Pure.proof", []);
-
-local
-
-val AbsPt = Const ("Pure.AbsP", propT --> (proofT --> proofT) --> proofT);
-val AppPt = Const ("Pure.AppP", proofT --> proofT --> proofT);
-val Hypt = Const ("Pure.Hyp", propT --> proofT);
-val Oraclet = Const ("Pure.Oracle", propT --> proofT);
-val MinProoft = Const ("Pure.MinProof", proofT);
-
-fun AppT T prf =
-  Const ("Pure.Appt", proofT --> Term.itselfT T --> proofT) $ prf $ Logic.mk_type T;
-
-fun OfClasst (T, c) =
-  let val U = Term.itselfT T --> propT
-  in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
-
-fun term_of _ (PThm ({serial = i, name, types = Ts, ...}, _)) =
-      fold AppT (these Ts)
-        (Const (Long_Name.append "thm" (if name = "" then string_of_int i else name), proofT))
-  | term_of _ (PAxm (name, _, Ts)) =
-      fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT))
-  | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c))
-  | term_of _ (PBound i) = Bound i
-  | term_of Ts (Abst (s, opT, prf)) =
-      let val T = the_default dummyT opT in
-        Const ("Pure.Abst", (T --> proofT) --> proofT) $
-          Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
-      end
-  | term_of Ts (AbsP (s, t, prf)) =
-      AbsPt $ the_default Term.dummy_prop t $
-        Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
-  | term_of Ts (prf1 %% prf2) =
-      AppPt $ term_of Ts prf1 $ term_of Ts prf2
-  | term_of Ts (prf % opt) =
-      let
-        val t = the_default Term.dummy opt;
-        val T = fastype_of1 (Ts, t) handle TERM _ => dummyT;
-      in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end
-  | term_of _ (Hyp t) = Hypt $ t
-  | term_of _ (Oracle (_, t, _)) = Oraclet $ t
-  | term_of _ MinProof = MinProoft;
-
-in
-
-val term_of_proof = term_of [];
-
-end;
-
-
-
 (** inference rules **)
 
 (* trivial implication *)