src/Pure/thm.ML
changeset 31943 5e960a0780a2
parent 31905 4263be178c8f
child 31944 c8a35979a5bc
     1.1 --- a/src/Pure/thm.ML	Sat Jul 04 23:25:28 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Mon Jul 06 19:58:52 2009 +0200
     1.3 @@ -1115,10 +1115,10 @@
     1.4    let
     1.5      val c = Sign.certify_class thy raw_c;
     1.6      val T = TVar ((Name.aT, 0), [c]);
     1.7 -    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_inclass (T, c))
     1.8 +    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c))
     1.9        handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    1.10    in
    1.11 -    Thm (deriv_rule0 (Pt.Inclass (T, c)),
    1.12 +    Thm (deriv_rule0 (Pt.OfClass (T, c)),
    1.13       {thy_ref = Theory.check_thy thy,
    1.14        tags = [],
    1.15        maxidx = maxidx,
    1.16 @@ -1137,7 +1137,7 @@
    1.17        raise THM ("unconstrainT: not a type variable", 0, [th]);
    1.18      val T' = TVar ((x, i), []);
    1.19      val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
    1.20 -    val constraints = map (curry Logic.mk_inclass T') S;
    1.21 +    val constraints = map (curry Logic.mk_of_class T') S;
    1.22    in
    1.23      Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
    1.24       {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),