src/Pure/Isar/code.ML
changeset 24969 b38527eefb3b
parent 24928 3419943838f5
child 25312 eb9067371342
     1.1 --- a/src/Pure/Isar/code.ML	Thu Oct 11 16:05:44 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Oct 11 16:05:47 2007 +0200
     1.3 @@ -545,8 +545,7 @@
     1.4  fun specific_constraints thy (class, tyco) =
     1.5    let
     1.6      val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
     1.7 -    val classparams = (map fst o these o Option.map snd
     1.8 -      o try (AxClass.params_of_class thy)) class;
     1.9 +    val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
    1.10      val funcs = classparams
    1.11        |> map (fn c => Class.inst_const thy (c, tyco))
    1.12        |> map (Symtab.lookup ((the_funcs o the_exec) thy))
    1.13 @@ -579,9 +578,9 @@
    1.14  
    1.15  fun gen_classparam_typ constr thy class (c, tyco) = 
    1.16    let
    1.17 -    val (var, cs) = try (AxClass.params_of_class thy) class |> the_default (Name.aT, [])
    1.18 +    val cs = these (try (#params o AxClass.get_info thy) class);
    1.19      val ty = (the o AList.lookup (op =) cs) c;
    1.20 -    val sort_args = Name.names (Name.declare var Name.context) Name.aT
    1.21 +    val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT
    1.22        (constr thy (class, tyco));
    1.23      val ty_inst = Type (tyco, map TFree sort_args);
    1.24    in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;