src/Pure/Isar/class.ML
changeset 24731 c25aa6ae64ec
parent 24707 dfeb98f84e93
child 24748 ee0a0eb6b738
     1.1 --- a/src/Pure/Isar/class.ML	Wed Sep 26 20:27:58 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Sep 26 20:50:33 2007 +0200
     1.3 @@ -255,8 +255,6 @@
     1.4       of [] => ()
     1.5        | dupl_tycos => error ("type constructors occur more than once in arities: "
     1.6            ^ (commas o map quote) dupl_tycos);
     1.7 -    val super_sort =
     1.8 -      (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory;
     1.9      fun get_consts_class tyco ty class =
    1.10        let
    1.11          val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
    1.12 @@ -268,7 +266,7 @@
    1.13        let
    1.14          val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
    1.15            (Name.names Name.context "'a" asorts))
    1.16 -      in maps (get_consts_class tyco ty) (super_sort sort) end;
    1.17 +      in maps (get_consts_class tyco ty) (Sign.complete_sort theory sort) end;
    1.18      val cs = maps get_consts_sort arities;
    1.19      fun mk_typnorm thy (ty, ty_sc) =
    1.20        case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
    1.21 @@ -418,7 +416,7 @@
    1.22      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
    1.23        (SOME o Pretty.str) ("class " ^ class ^ ":"),
    1.24        (SOME o Pretty.block) [Pretty.str "supersort: ",
    1.25 -        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
    1.26 +        (Sign.pretty_sort thy o Sign.minimize_sort thy o Sign.super_classes thy) class],
    1.27        Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
    1.28        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
    1.29          o these o Option.map #params o try (AxClass.get_definition thy)) class,
    1.30 @@ -575,8 +573,8 @@
    1.31        | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
    1.32      val supclasses = map (prep_class thy) raw_supclasses;
    1.33      val sups = filter (is_some o lookup_class_data thy) supclasses
    1.34 -      |> Sign.certify_sort thy;
    1.35 -    val supsort = Sign.certify_sort thy supclasses;
    1.36 +      |> Sign.minimize_sort thy;
    1.37 +    val supsort = Sign.minimize_sort thy supclasses;
    1.38      val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
    1.39      val supexpr = Locale.Merge (suplocales @ includes);
    1.40      val supparams = (map fst o Locale.parameters_of_expr thy)
    1.41 @@ -721,8 +719,7 @@
    1.42      val loc_expr = (Locale.Locale o #locale o the_class_data theory) superclass;
    1.43      fun prove_classrel (class, superclass) thy =
    1.44        let
    1.45 -        val classes = (Graph.all_succs o #classes o Sorts.rep_algebra
    1.46 -              o Sign.classes_of) thy [superclass]
    1.47 +        val classes = Sign.complete_sort thy [superclass]
    1.48            |> filter_out (fn class' => Sign.subsort thy ([class], [class']));
    1.49          fun instance_subclass (class1, class2) thy  =
    1.50            let
    1.51 @@ -731,7 +728,7 @@
    1.52              val intro = #intro (AxClass.get_definition thy class2)
    1.53                |> Drule.instantiate' [SOME (Thm.ctyp_of thy
    1.54                    (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
    1.55 -            val thm = 
    1.56 +            val thm =
    1.57                intro
    1.58                |> OF_LAST (interp OF ax)
    1.59                |> strip_all_ofclass thy (Sign.super_classes thy class2);