1.1 --- a/src/Pure/Isar/code.ML	Sat Nov 27 19:41:27 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Sat Nov 27 19:41:28 2010 +0100
     1.3 @@ -742,16 +742,16 @@
     1.4  
     1.5  fun empty_cert thy c = 
     1.6    let
     1.7 -    val raw_ty = const_typ thy c;
     1.8 -    val tvars = Term.add_tvar_namesT raw_ty [];
     1.9 -    val tvars' = case AxClass.class_of_param thy c
    1.10 -     of SOME class => [TFree (Name.aT, [class])]
    1.11 -      | NONE =>  (case get_type_of_constr_or_abstr thy c
    1.12 -         of SOME (tyco, _) => map TFree ((fst o the)
    1.13 -              (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c))
    1.14 -          | NONE => Name.invent_list [] Name.aT (length tvars)
    1.15 -              |> map (fn v => TFree (v, [])));
    1.16 -    val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
    1.17 +    val raw_ty = Logic.unvarifyT_global (const_typ thy c);
    1.18 +    val (vs, _) = typscheme thy (c, raw_ty);
    1.19 +    val sortargs = case AxClass.class_of_param thy c
    1.20 +     of SOME class => [[class]]
    1.21 +      | NONE => (case get_type_of_constr_or_abstr thy c
    1.22 +         of SOME (tyco, _) => (map snd o fst o the)
    1.23 +              (AList.lookup (op =) ((snd o fst o get_type thy) tyco) c)
    1.24 +          | NONE => replicate (length vs) []);
    1.25 +    val the_sort = the o AList.lookup (op =) (map fst vs ~~ sortargs);
    1.26 +    val ty = map_type_tfree (fn (v, _) => TFree (v, the_sort v)) raw_ty
    1.27      val chead = build_head thy (c, ty);
    1.28    in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
    1.29