1.1 --- a/src/Tools/code/code_thingol.ML	Mon Dec 01 12:17:01 2008 +0100
     1.2 +++ b/src/Tools/code/code_thingol.ML	Mon Dec 01 12:17:02 2008 +0100
     1.3 @@ -489,7 +489,7 @@
     1.4  
     1.5  fun ensure_class thy (algbr as (_, algebra)) funcgr class =
     1.6    let
     1.7 -    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
     1.8 +    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     1.9      val cs = #params (AxClass.get_info thy class);
    1.10      val stmt_class =
    1.11        fold_map (fn superclass => ensure_class thy algbr funcgr superclass
    1.12 @@ -538,8 +538,16 @@
    1.13            Global ((class, tyco), yss)
    1.14        | class_relation (Local (classrels, v), subclass) superclass =
    1.15            Local ((subclass, superclass) :: classrels, v);
    1.16 +    fun norm_typargs ys =
    1.17 +      let
    1.18 +        val raw_sort = map snd ys;
    1.19 +        val sort = Sorts.minimize_sort algebra raw_sort;
    1.20 +      in
    1.21 +        map_filter (fn (y, class) =>
    1.22 +          if member (op =) sort class then SOME y else NONE) ys
    1.23 +      end;
    1.24      fun type_constructor tyco yss class =
    1.25 -      Global ((class, tyco), (map o map) fst yss);
    1.26 +      Global ((class, tyco), map norm_typargs yss);
    1.27      fun type_variable (TFree (v, sort)) =
    1.28        let
    1.29          val sort' = proj_sort sort;
    1.30 @@ -567,7 +575,7 @@
    1.31    end
    1.32  and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) =
    1.33    let
    1.34 -    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
    1.35 +    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    1.36      val classparams = these (try (#params o AxClass.get_info thy) class);
    1.37      val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
    1.38      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
    1.39 @@ -736,9 +744,9 @@
    1.40  
    1.41  val cached_program = Program.get;
    1.42  
    1.43 -fun invoke_generation thy funcgr f name =
    1.44 +fun invoke_generation thy (algebra, funcgr) f name =
    1.45    Program.change_yield thy (fn naming_program => (NONE, naming_program)
    1.46 -    |> f thy (Code.operational_algebra thy) funcgr name
    1.47 +    |> f thy algebra funcgr name
    1.48      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
    1.49  
    1.50  
    1.51 @@ -789,9 +797,10 @@
    1.52  fun eval thy evaluator t =
    1.53    let
    1.54      val (t', evaluator'') = evaluator t;
    1.55 -    fun evaluator' funcgr =
    1.56 +    fun evaluator' algebra funcgr =
    1.57        let
    1.58 -        val (((naming, program), (vs_ty_t, deps)), _) = invoke_generation thy funcgr ensure_value t';
    1.59 +        val (((naming, program), (vs_ty_t, deps)), _) =
    1.60 +          invoke_generation thy (algebra, funcgr) ensure_value t';
    1.61        in evaluator'' naming program vs_ty_t deps end;
    1.62    in (t', evaluator') end
    1.63