src/Pure/thm.ML
changeset 31903 c5221dbc40f6
parent 30717 465093aa5844
child 31905 4263be178c8f
     1.1 --- a/src/Pure/thm.ML	Thu Jul 02 17:34:14 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Jul 02 20:55:44 2009 +0200
     1.3 @@ -1110,15 +1110,21 @@
     1.4        prop = Logic.mk_implies (A, A)});
     1.5  
     1.6  (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
     1.7 -fun class_triv thy c =
     1.8 +fun class_triv thy raw_c =
     1.9    let
    1.10 -    val Cterm {t, maxidx, sorts, ...} =
    1.11 -      cterm_of thy (Logic.mk_inclass (TVar ((Name.aT, 0), [c]), Sign.certify_class thy c))
    1.12 -        handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    1.13 -    val der = deriv_rule0 (Pt.PAxm ("Pure.class_triv:" ^ c, t, SOME []));
    1.14 +    val c = Sign.certify_class thy raw_c;
    1.15 +    val T = TVar ((Name.aT, 0), [c]);
    1.16 +    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (T, c))
    1.17 +      handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    1.18    in
    1.19 -    Thm (der, {thy_ref = Theory.check_thy thy, tags = [], maxidx = maxidx,
    1.20 -      shyps = sorts, hyps = [], tpairs = [], prop = t})
    1.21 +    Thm (deriv_rule0 (Pt.Inclass (T, c)),
    1.22 +     {thy_ref = Theory.check_thy thy,
    1.23 +      tags = [],
    1.24 +      maxidx = maxidx,
    1.25 +      shyps = sorts,
    1.26 +      hyps = [],
    1.27 +      tpairs = [],
    1.28 +      prop = prop})
    1.29    end;
    1.30  
    1.31  (*Internalize sort constraints of type variable*)