765 |
765 |
766 val AbsPt = Const ("Pure.AbsP", [propT, proofT --> proofT] ---> proofT); |
766 val AbsPt = Const ("Pure.AbsP", [propT, proofT --> proofT] ---> proofT); |
767 val AppPt = Const ("Pure.AppP", [proofT, proofT] ---> proofT); |
767 val AppPt = Const ("Pure.AppP", [proofT, proofT] ---> proofT); |
768 val Hypt = Const ("Pure.Hyp", propT --> proofT); |
768 val Hypt = Const ("Pure.Hyp", propT --> proofT); |
769 val Oraclet = Const ("Pure.Oracle", propT --> proofT); |
769 val Oraclet = Const ("Pure.Oracle", propT --> proofT); |
770 val OfClasst = Const ("Pure.OfClass", (Term.itselfT dummyT --> propT) --> proofT); |
|
771 val MinProoft = Const ("Pure.MinProof", proofT); |
770 val MinProoft = Const ("Pure.MinProof", proofT); |
|
771 |
|
772 fun OfClasst (T, c) = |
|
773 let val U = Term.itselfT T --> propT |
|
774 in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end; |
772 |
775 |
773 val mk_tyapp = fold (fn T => fn prf => Const ("Pure.Appt", |
776 val mk_tyapp = fold (fn T => fn prf => Const ("Pure.Appt", |
774 [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); |
777 [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); |
775 |
778 |
776 fun term_of _ (PThm (_, ((name, _, NONE), _))) = |
779 fun term_of _ (PThm (_, ((name, _, NONE), _))) = |
778 | term_of _ (PThm (_, ((name, _, SOME Ts), _))) = |
781 | term_of _ (PThm (_, ((name, _, SOME Ts), _))) = |
779 mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT)) |
782 mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT)) |
780 | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) |
783 | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) |
781 | term_of _ (PAxm (name, _, SOME Ts)) = |
784 | term_of _ (PAxm (name, _, SOME Ts)) = |
782 mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT)) |
785 mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT)) |
783 | term_of _ (OfClass (T, c)) = |
786 | term_of _ (OfClass (T, c)) = mk_tyapp [T] (OfClasst (T, c)) |
784 mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT)) |
|
785 | term_of _ (PBound i) = Bound i |
787 | term_of _ (PBound i) = Bound i |
786 | term_of Ts (Abst (s, opT, prf)) = |
788 | term_of Ts (Abst (s, opT, prf)) = |
787 let val T = the_default dummyT opT |
789 let val T = the_default dummyT opT |
788 in Const ("Pure.Abst", (T --> proofT) --> proofT) $ |
790 in Const ("Pure.Abst", (T --> proofT) --> proofT) $ |
789 Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) |
791 Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) |