# HG changeset patch
# User wenzelm
# Date 1563715147 -7200
# Node ID e31271559de844c454d3e49b9693980696a8d0ce
# Parent  35dd9212bf295c468667dc64040d8d43a96b8944
global declaration of abstract syntax for proof terms, with qualified names;
clarified modules;

diff -r 35dd9212bf29 -r e31271559de8 src/HOL/Tools/rewrite_hol_proof.ML
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Sun Jul 21 12:28:02 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Sun Jul 21 15:19:07 2019 +0200
@@ -34,9 +34,9 @@
    \<open>(meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> x1 \<cdot> x2 \<bullet> prfU \<bullet>
       (combination \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet> prf1 \<bullet> prf2)) \<equiv>
     (cong \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet>
-      (OfClass type_class \<cdot> TYPE('T)) \<bullet> prfU \<bullet>
-      (meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> f \<cdot> g \<bullet> (OfClass type_class \<cdot> TYPE('T \<Rightarrow> 'U)) \<bullet> prf1) \<bullet>
-      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> (OfClass type_class \<cdot> TYPE('T)) \<bullet> prf2))\<close>,
+      (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> prfU \<bullet>
+      (meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> f \<cdot> g \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T \<Rightarrow> 'U)) \<bullet> prf1) \<bullet>
+      (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> prf2))\<close>,
 
    \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet>
       (axm.transitive \<cdot> TYPE('T) \<cdot> x \<cdot> y \<cdot> z \<bullet> prf1 \<bullet> prf2)) \<equiv>
@@ -54,9 +54,9 @@
    \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> x1 \<cdot> x2 \<bullet> prfTU \<bullet>
       (abstract_rule \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet> prf)) \<equiv>
     (ext \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet>
-      (OfClass type_class \<cdot> TYPE('T)) \<bullet> (OfClass type_class \<cdot> TYPE('U)) \<bullet>
+      (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> (Pure.OfClass type_class \<cdot> TYPE('U)) \<bullet>
       (\<^bold>\<lambda>(x::'T). meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> f x \<cdot> g x \<bullet>
-         (OfClass type_class \<cdot> TYPE('U)) \<bullet> (prf \<cdot> x)))\<close>,
+         (Pure.OfClass type_class \<cdot> TYPE('U)) \<bullet> (prf \<cdot> x)))\<close>,
 
    \<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet>
       (eq_reflection \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf)) \<equiv> prf\<close>,
@@ -70,9 +70,9 @@
         prfT \<bullet> arity_type_bool \<bullet>
         (cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
           ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
-          prfT \<bullet> (OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
+          prfT \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
           (HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
-             (OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
+             (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
           (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
         (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
       (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> C \<bullet> prfT \<bullet> prf3))\<close>,
@@ -87,9 +87,9 @@
         prfT \<bullet> arity_type_bool \<bullet>
         (cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
           ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
-          prfT \<bullet> (OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
+          prfT \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
           (HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
-             (OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
+             (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
           (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
         (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
       (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> B \<cdot> D \<bullet> prfT \<bullet> prf3))\<close>,
@@ -155,7 +155,7 @@
         ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
           prfb \<bullet> prfbb \<bullet>
           (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
-             (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
           (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
 
    (* \<or> *)
@@ -181,7 +181,7 @@
         ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
           prfb \<bullet> prfbb \<bullet>
           (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
-             (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
           (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
 
    (* \<longrightarrow> *)
@@ -205,7 +205,7 @@
         ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
           prfb \<bullet> prfbb \<bullet>
           (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
-             (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
           (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
 
    (* \<not> *)
@@ -257,7 +257,7 @@
         ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
           prfb \<bullet> prfbb \<bullet>
           (HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
-             (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+             (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
           (HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
 
    (** transitivity, reflexivity, and symmetry **)
diff -r 35dd9212bf29 -r e31271559de8 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Jul 21 15:19:07 2019 +0200
@@ -6,10 +6,8 @@
 
 signature PROOF_SYNTAX =
 sig
-  val proofT: typ
   val add_proof_syntax: theory -> theory
   val proof_of_term: theory -> bool -> term -> Proofterm.proof
-  val term_of_proof: Proofterm.proof -> term
   val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
   val read_term: theory -> bool -> typ -> string -> term
   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
@@ -24,40 +22,23 @@
 
 (**** add special syntax for embedding proof terms ****)
 
-val proofT = Type ("proof", []);
+val proofT = Proofterm.proofT;
+
+local
+
 val paramT = Type ("param", []);
 val paramsT = Type ("params", []);
 val idtT = Type ("idt", []);
 val aT = Term.aT [];
 
-
-(** constants for theorems and axioms **)
+fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
 
-fun add_proof_atom_consts names thy =
-  thy
-  |> Sign.root_path
-  |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
-
-
-(** constants for application and abstraction **)
-
-fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
+in
 
 fun add_proof_syntax thy =
   thy
   |> Sign.root_path
   |> Sign.set_defsort []
-  |> Sign.add_types_global
-    [(Binding.make ("proof", \<^here>), 0, NoSyn)]
-  |> fold (snd oo Sign.declare_const_global)
-    [((Binding.make ("Appt", \<^here>), [proofT, aT] ---> proofT), mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
-     ((Binding.make ("AppP", \<^here>), [proofT, proofT] ---> proofT), mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
-     ((Binding.make ("Abst", \<^here>), (aT --> proofT) --> proofT), NoSyn),
-     ((Binding.make ("AbsP", \<^here>), [propT, proofT --> proofT] ---> proofT), NoSyn),
-     ((Binding.make ("Hyp", \<^here>), propT --> proofT), NoSyn),
-     ((Binding.make ("Oracle", \<^here>), propT --> proofT), NoSyn),
-     ((Binding.make ("OfClass", \<^here>), (Term.a_itselfT --> propT) --> proofT), NoSyn),
-     ((Binding.make ("MinProof", \<^here>), proofT), Mixfix.mixfix "?")]
   |> Sign.add_nonterminals_global
     [Binding.make ("param", \<^here>),
      Binding.make ("params", \<^here>)]
@@ -68,11 +49,14 @@
      ("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)),
      ("", paramT --> paramT, Mixfix.mixfix "'(_')"),
      ("", idtT --> paramsT, Mixfix.mixfix "_"),
-     ("", paramT --> paramsT, Mixfix.mixfix "_")]
+     ("", paramT --> paramsT, Mixfix.mixfix "_"),
+     (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+     (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
+     (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "?")]
   |> Sign.add_syntax (Print_Mode.ASCII, true)
     [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)),
-     (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
-     (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
+     (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
+     (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
   |> Sign.add_trrules (map Syntax.Parse_Print_Rule
     [(Ast.mk_appl (Ast.Constant "_Lam")
         [Ast.mk_appl (Ast.Constant "_Lam0")
@@ -83,12 +67,22 @@
      (Ast.mk_appl (Ast.Constant "_Lam")
         [Ast.mk_appl (Ast.Constant "_Lam1")
           [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
-      Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
+      Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.AbsP")) [Ast.Variable "A",
         (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
      (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
-      Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
+      Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.Abst"))
         [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
 
+end;
+
+
+(** constants for theorems and axioms **)
+
+fun add_proof_atom_consts names thy =
+  thy
+  |> Sign.root_path
+  |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
+
 
 (**** translation between proof terms and pure terms ****)
 
@@ -101,7 +95,7 @@
       (Term.no_dummy_patterns t);
 
     fun prf_of [] (Bound i) = PBound i
-      | prf_of Ts (Const (s, Type ("proof", _))) =
+      | prf_of Ts (Const (s, Type ("Pure.proof", _))) =
           Proofterm.change_type (if ty then SOME Ts else NONE)
             (case Long_Name.explode s of
                "axm" :: xs =>
@@ -119,30 +113,30 @@
                    | NONE => error ("Unknown theorem " ^ quote name))
                  end
              | _ => error ("Illegal proof constant name: " ^ quote s))
-      | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) =
+      | prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) =
           (case try Logic.class_of_const c_class of
             SOME c =>
               Proofterm.change_type (if ty then SOME Ts else NONE)
                 (OfClass (TVar ((Name.aT, 0), []), c))
           | NONE => error ("Bad class constant: " ^ quote c_class))
-      | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
-      | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
-      | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
+      | prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop
+      | prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v
+      | prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) =
           if T = proofT then
             error ("Term variable abstraction may not bind proof variable " ^ quote s)
           else Abst (s, if ty then SOME T else NONE,
             Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
-      | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
+      | prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) =
           AbsP (s, case t of
                 Const ("Pure.dummy_pattern", _) => NONE
               | _ $ Const ("Pure.dummy_pattern", _) => NONE
               | _ => SOME (mk_term t),
             Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
-      | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
+      | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) =
           prf_of [] prf1 %% prf_of [] prf2
-      | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
+      | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
           prf_of (T::Ts) prf
-      | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
+      | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf %
           (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
       | prf_of _ t = error ("Not a proof term:\n" ^
           Syntax.string_of_term_global thy t)
@@ -150,48 +144,6 @@
   in prf_of [] end;
 
 
-val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
-val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
-val Hypt = Const ("Hyp", propT --> proofT);
-val Oraclet = Const ("Oracle", propT --> proofT);
-val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT);
-val MinProoft = Const ("MinProof", proofT);
-
-val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
-  [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
-
-fun term_of _ (PThm (_, ((name, _, NONE), _))) =
-      Const (Long_Name.append "thm" name, proofT)
-  | term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
-      mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
-  | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
-  | term_of _ (PAxm (name, _, SOME Ts)) =
-      mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
-  | term_of _ (OfClass (T, c)) =
-      mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
-  | term_of _ (PBound i) = Bound i
-  | term_of Ts (Abst (s, opT, prf)) =
-      let val T = the_default dummyT opT
-      in Const ("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
-      in Const ("Appt",
-        [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
-          term_of Ts prf $ t
-      end
-  | term_of Ts (Hyp t) = Hypt $ t
-  | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
-  | term_of Ts MinProof = MinProoft;
-
-val term_of_proof = term_of [];
-
 fun cterm_of_proof thy prf =
   let
     val thm_names = map fst (Global_Theory.all_thms_of thy true);
@@ -201,7 +153,7 @@
       |> add_proof_atom_consts
         (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
   in
-    (Thm.global_cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
+    (Thm.global_cterm_of thy' (Proofterm.term_of_proof prf), proof_of_term thy true o Thm.term_of)
   end;
 
 fun read_term thy topsort =
@@ -257,7 +209,7 @@
 fun pretty_proof ctxt prf =
   Proof_Context.pretty_term_abbrev
     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
-    (term_of_proof prf);
+    (Proofterm.term_of_proof prf);
 
 fun pretty_clean_proof_of ctxt full thm =
   pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm);
diff -r 35dd9212bf29 -r e31271559de8 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/proofterm.ML	Sun Jul 21 15:19:07 2019 +0200
@@ -91,6 +91,8 @@
   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 implies_intr_proof: term -> proof -> proof
@@ -755,6 +757,59 @@
 end;
 
 
+(**** 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 OfClasst = Const ("Pure.OfClass", (Term.itselfT dummyT --> propT) --> proofT);
+val MinProoft = Const ("Pure.MinProof", proofT);
+
+val mk_tyapp = fold (fn T => fn prf => Const ("Pure.Appt",
+  [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
+
+fun term_of _ (PThm (_, ((name, _, NONE), _))) =
+      Const (Long_Name.append "thm" name, proofT)
+  | term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
+      mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
+  | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
+  | term_of _ (PAxm (name, _, SOME Ts)) =
+      mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
+  | term_of _ (OfClass (T, c)) =
+      mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
+  | 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
+      in Const ("Pure.Appt",
+        [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
+          term_of Ts prf $ t
+      end
+  | term_of Ts (Hyp t) = Hypt $ t
+  | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
+  | term_of Ts MinProof = MinProoft;
+
+in
+
+val term_of_proof = term_of [];
+
+end;
+
+
 (***** implication introduction *****)
 
 fun gen_implies_intr_proof f h prf =
diff -r 35dd9212bf29 -r e31271559de8 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/pure_thy.ML	Sun Jul 21 15:19:07 2019 +0200
@@ -14,6 +14,8 @@
 structure Pure_Thy: PURE_THY =
 struct
 
+(* auxiliary *)
+
 val typ = Simple_Syntax.read_typ;
 val prop = Simple_Syntax.read_prop;
 
@@ -27,6 +29,18 @@
 fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
 fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
 
+fun add_deps_type c thy =
+  let
+    val n = Sign.arity_number thy c;
+    val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+  in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end
+
+fun add_deps_const c thy =
+  let
+    val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
+    val typargs = Sign.const_typargs thy (c, T);
+  in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end;
+
 
 (* application syntax variants *)
 
@@ -70,11 +84,13 @@
    [(Binding.make ("fun", \<^here>), 2, NoSyn),
     (Binding.make ("prop", \<^here>), 0, NoSyn),
     (Binding.make ("itself", \<^here>), 1, NoSyn),
-    (Binding.make ("dummy", \<^here>), 0, NoSyn)]
-  #> Theory.add_deps_global "fun" ((Defs.Type, "fun"), [typ "'a", typ "'b"]) []
-  #> Theory.add_deps_global "prop" ((Defs.Type, "prop"), []) []
-  #> Theory.add_deps_global "itself" ((Defs.Type, "itself"), [typ "'a"]) []
-  #> Theory.add_deps_global "dummy" ((Defs.Type, "dummy"), []) []
+    (Binding.make ("dummy", \<^here>), 0, NoSyn),
+    (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)]
+  #> add_deps_type "fun"
+  #> add_deps_type "prop"
+  #> add_deps_type "itself"
+  #> add_deps_type "dummy"
+  #> add_deps_type "Pure.proof"
   #> Sign.add_nonterminals_global
     (map (fn name => Binding.make (name, \<^here>))
       (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
@@ -200,12 +216,20 @@
     (qualify (Binding.make ("all", \<^here>)), typ "('a \<Rightarrow> prop) \<Rightarrow> prop", binder ("\<And>", 0, 0)),
     (qualify (Binding.make ("prop", \<^here>)), typ "prop \<Rightarrow> prop", NoSyn),
     (qualify (Binding.make ("type", \<^here>)), typ "'a itself", NoSyn),
-    (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_")]
-  #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
-  #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
-  #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []
-  #> Theory.add_deps_global "Pure.type" ((Defs.Const, "Pure.type"), [typ "'a"]) []
-  #> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Const, "Pure.dummy_pattern"), [typ "'a"]) []
+    (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_"),
+    (qualify (Binding.make ("Appt", \<^here>)), typ "Pure.proof \<Rightarrow> 'a \<Rightarrow> Pure.proof", NoSyn),
+    (qualify (Binding.make ("AppP", \<^here>)), typ "Pure.proof \<Rightarrow> Pure.proof \<Rightarrow> Pure.proof", NoSyn),
+    (qualify (Binding.make ("Abst", \<^here>)), typ "('a \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn),
+    (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn),
+    (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
+    (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
+    (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
+    (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", Mixfix.mixfix "?")]
+  #> add_deps_const "Pure.eq"
+  #> add_deps_const "Pure.imp"
+  #> add_deps_const "Pure.all"
+  #> add_deps_const "Pure.type"
+  #> add_deps_const "Pure.dummy_pattern"
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
diff -r 35dd9212bf29 -r e31271559de8 src/Pure/pure_thy.scala
--- a/src/Pure/pure_thy.scala	Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/pure_thy.scala	Sun Jul 21 15:19:07 2019 +0200
@@ -22,16 +22,16 @@
   val TYPE: String = "Pure.type"
 
 
-  /* proof terms (abstract syntax) */
+  /* abstract syntax for proof terms */
 
-  val PROOF: String = "proof"
+  val PROOF: String = "Pure.proof"
 
-  val APPT: String = "Appt"
-  val APPP: String = "AppP"
-  val ABST: String = "Abst"
-  val ABSP: String = "AbsP"
-  val HYP: String = "Hyp"
-  val ORACLE: String = "Oracle"
-  val OFCLASS: String = "OfClass"
-  val MINPROOF: String = "MinProof"
+  val APPT: String = "Pure.Appt"
+  val APPP: String = "Pure.AppP"
+  val ABST: String = "Pure.Abst"
+  val ABSP: String = "Pure.AbsP"
+  val HYP: String = "Pure.Hyp"
+  val ORACLE: String = "Pure.Oracle"
+  val OFCLASS: String = "Pure.OfClass"
+  val MINPROOF: String = "Pure.MinProof"
 }