--- a/src/Pure/thm.ML Thu Oct 04 20:29:13 2007 +0200
+++ b/src/Pure/thm.ML Thu Oct 04 20:29:24 2007 +0200
@@ -1144,7 +1144,7 @@
fun class_triv thy c =
let
val Cterm {t, maxidx, sorts, ...} =
- cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c))
+ cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
val der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME []));
in