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