src/Pure/thm.ML
changeset 24848 5dbbd33c3236
parent 24313 5a6342236a32
child 25939 ddea202704b4
     1.1 --- a/src/Pure/thm.ML	Thu Oct 04 20:29:13 2007 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Oct 04 20:29:24 2007 +0200
     1.3 @@ -1144,7 +1144,7 @@
     1.4  fun class_triv thy c =
     1.5    let
     1.6      val Cterm {t, maxidx, sorts, ...} =
     1.7 -      cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), Sign.certify_class thy c))
     1.8 +      cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
     1.9          handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    1.10      val der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME []));
    1.11    in