(continued)
authorhaftmann
Thu Mar 20 12:01:16 2008 +0100 (2008-03-20)
changeset 26353537ff6997149
parent 26352 7f50b708376c
child 26354 46c7d00dd4b4
(continued)
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Mar 20 12:01:14 2008 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Mar 20 12:01:16 2008 +0100
     1.3 @@ -599,7 +599,7 @@
     1.4      ||>> get_axiom
     1.5      |-> (fn (def, def') => class_interpretation class [def] [Thm.prop_of def]
     1.6        #> register_operation class (c', (dict', SOME (Thm.symmetric def')))
     1.7 -      #> PureThy.note Thm.internalK (c, def')
     1.8 +      #> PureThy.note Thm.internalK (c ^ "_raw", def')
     1.9        #> snd)
    1.10      |> Sign.restore_naming thy
    1.11      |> Sign.add_const_constraint (c', SOME ty')
    1.12 @@ -716,17 +716,18 @@
    1.13      val local_constraints = map (apsnd (subst_class_typ []) o snd) params;
    1.14      val pseudo_constraints = map (fn (_, (c, _)) => (c, class_of c)) params;
    1.15      val typ_of_sort = Type.typ_of_sort (Sign.classes_of thy);
    1.16 -    val typarg = the_single o Sign.const_typargs thy;
    1.17 +    val typargs = Sign.const_typargs thy;
    1.18      val pp = Sign.pp thy;
    1.19 -    fun constrain_class (c, ty) class =
    1.20 +    fun constrain_typ tys sorts ty =
    1.21        let
    1.22 -        val ty' = typarg (c, ty);
    1.23 -        val tyenv = typ_of_sort ty' [class] Vartab.empty
    1.24 +        val tyenv = fold2 typ_of_sort tys sorts Vartab.empty
    1.25            handle Sorts.CLASS_ERROR e => Sorts.class_error pp e;
    1.26        in
    1.27          map_atyps (fn TVar (vi, _) => TVar (vi, the (Vartab.lookup tyenv vi))
    1.28            | ty => ty) ty
    1.29        end;
    1.30 +    fun constrain_class (c, ty) class =
    1.31 +      constrain_typ (typargs (c, ty)) [[class]] ty;
    1.32      fun improve_param (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.33       of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
    1.34           of SOME (_, ty') => SOME (ty, ty')