# HG changeset patch
# User wenzelm
# Date 1146495913 -7200
# Node ID 0cd0bf32ac58c5a7d327ba01d55c82352f8bbaa1
# Parent  f795c11647082b5fa6bb7b1a30f037a7c3d8e33e
class_triv: Sign.certify_class;

diff -r f795c1164708 -r 0cd0bf32ac58 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon May 01 17:05:12 2006 +0200
+++ b/src/Pure/thm.ML	Mon May 01 17:05:13 2006 +0200
@@ -1066,7 +1066,7 @@
 (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
 fun class_triv thy c =
   let val Cterm {thy_ref, t, maxidx, sorts, ...} =
-    cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
+    cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c))
       handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
   in
     Thm {thy_ref = thy_ref,