--- a/src/Pure/Proof/proof_syntax.ML Thu Jul 02 17:34:14 2009 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Thu Jul 02 20:55:44 2009 +0200
@@ -54,6 +54,7 @@
(Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT, NoSyn),
(Binding.name "Hyp", propT --> proofT, NoSyn),
(Binding.name "Oracle", propT --> proofT, NoSyn),
+ (Binding.name "Inclass", (Term.a_itselfT --> propT) --> proofT, NoSyn),
(Binding.name "MinProof", proofT, Delimfix "?")]
|> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
|> Sign.add_syntax_i
@@ -112,6 +113,12 @@
| NONE => error ("Unknown theorem " ^ quote name))
end
| _ => error ("Illegal proof constant name: " ^ quote s))
+ | prf_of Ts (Const ("Inclass", _) $ Const (c_class, _)) =
+ (case try Logic.class_of_const c_class of
+ SOME c =>
+ change_type (if ty then SOME Ts else NONE)
+ (Inclass (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)) =
@@ -141,6 +148,7 @@
val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
val Hypt = Const ("Hyp", propT --> proofT);
val Oraclet = Const ("Oracle", propT --> proofT);
+val Inclasst = Const ("Inclass", (Term.itselfT dummyT --> propT) --> proofT);
val MinProoft = Const ("MinProof", proofT);
val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
@@ -153,6 +161,8 @@
| 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 _ (Inclass (T, c)) =
+ mk_tyapp [T] (Inclasst $ 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