# HG changeset patch
# User berghofe
# Date 1022863943 -7200
# Node ID 18402c1f76bf99e5e6012f10fbbdc0c1ee89b2e5
# Parent  3e40f48a500fe59c5c988f09c8f547ae384d3f4f
Added constants for Hyp, Oracle and MinProof.

diff -r 3e40f48a500f -r 18402c1f76bf src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri May 31 18:50:03 2002 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri May 31 18:52:23 2002 +0200
@@ -56,7 +56,10 @@
       [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
        ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
        ("Abst", (aT --> proofT) --> proofT, NoSyn),
-       ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn)]
+       ("AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
+       ("Hyp", propT --> proofT, NoSyn),
+       ("Oracle", propT --> proofT, NoSyn),
+       ("MinProof", proofT, Delimfix "?")]
   |> Sign.add_nonterminals ["param", "params"]
   |> Sign.add_syntax_i
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
@@ -150,6 +153,7 @@
                        | None => error ("Unknown theorem " ^ quote name)))
                  end
              | _ => error ("Illegal proof constant name: " ^ quote s))
+      | 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)) =
           Abst (s, if ty then Some T else None,
@@ -174,9 +178,9 @@
 
 val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
 val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
-val Hypt = Free ("Hyp", propT --> proofT);
-val Oraclet = Free ("Oracle", propT --> proofT);
-val MinProoft = Free ("?", proofT);
+val Hypt = Const ("Hyp", propT --> proofT);
+val Oraclet = Const ("Oracle", propT --> proofT);
+val MinProoft = Const ("MinProof", proofT);
 
 val mk_tyapp = foldl (fn (prf, T) => Const ("Appt",
   [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);