# HG changeset patch
# User wenzelm
# Date 1563786608 -7200
# Node ID 47fd6c7b9559b10694a79094136ad088a11a61f3
# Parent  772321761cb8516ef1033b47f3b3e90b5fa49b17
more accurate type information;

diff -r 772321761cb8 -r 47fd6c7b9559 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Jul 22 11:09:24 2019 +0200
+++ b/src/Pure/proofterm.ML	Mon Jul 22 11:10:08 2019 +0200
@@ -767,9 +767,12 @@
 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);
 
+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;
+
 val mk_tyapp = fold (fn T => fn prf => Const ("Pure.Appt",
   [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
 
@@ -780,8 +783,7 @@
   | 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 _ (OfClass (T, c)) = mk_tyapp [T] (OfClasst (T, c))
   | term_of _ (PBound i) = Bound i
   | term_of Ts (Abst (s, opT, prf)) =
       let val T = the_default dummyT opT