src/Pure/thm.ML
changeset 31944 c8a35979a5bc
parent 31943 5e960a0780a2
child 31945 d5f186aa0bed
     1.1 --- a/src/Pure/thm.ML	Mon Jul 06 19:58:52 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Mon Jul 06 20:36:38 2009 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4    val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
     1.5    val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
     1.6    val trivial: cterm -> thm
     1.7 -  val class_triv: theory -> class -> thm
     1.8 +  val of_class: ctyp * class -> thm
     1.9    val unconstrainT: ctyp -> thm -> thm
    1.10    val dest_state: thm * int -> (term * term) list * term list * term * term
    1.11    val lift_rule: cterm -> thm -> thm
    1.12 @@ -1110,22 +1110,28 @@
    1.13        tpairs = [],
    1.14        prop = Logic.mk_implies (A, A)});
    1.15  
    1.16 -(*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
    1.17 -fun class_triv thy raw_c =
    1.18 +(*Axiom-scheme reflecting signature contents
    1.19 +        T :: c
    1.20 +  -------------------
    1.21 +  OFCLASS(T, c_class)
    1.22 +*)
    1.23 +fun of_class (cT, raw_c) =
    1.24    let
    1.25 +    val Ctyp {thy_ref, T, ...} = cT;
    1.26 +    val thy = Theory.deref thy_ref;
    1.27      val c = Sign.certify_class thy raw_c;
    1.28 -    val T = TVar ((Name.aT, 0), [c]);
    1.29 -    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c))
    1.30 -      handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
    1.31 +    val Cterm {t = prop, maxidx, sorts, ...} = cterm_of thy (Logic.mk_of_class (T, c));
    1.32    in
    1.33 -    Thm (deriv_rule0 (Pt.OfClass (T, c)),
    1.34 -     {thy_ref = Theory.check_thy thy,
    1.35 -      tags = [],
    1.36 -      maxidx = maxidx,
    1.37 -      shyps = sorts,
    1.38 -      hyps = [],
    1.39 -      tpairs = [],
    1.40 -      prop = prop})
    1.41 +    if Sign.of_sort thy (T, [c]) then
    1.42 +      Thm (deriv_rule0 (Pt.OfClass (T, c)),
    1.43 +       {thy_ref = Theory.check_thy thy,
    1.44 +        tags = [],
    1.45 +        maxidx = maxidx,
    1.46 +        shyps = sorts,
    1.47 +        hyps = [],
    1.48 +        tpairs = [],
    1.49 +        prop = prop})
    1.50 +    else raise THM ("of_class: type not of class " ^ Syntax.string_of_sort_global thy [c], 0, [])
    1.51    end;
    1.52  
    1.53  (*Internalize sort constraints of type variable*)