1.1 --- a/src/Pure/Isar/class_target.ML	Wed Feb 18 19:18:31 2009 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Wed Feb 18 19:18:32 2009 +0100
     1.3 @@ -493,7 +493,7 @@
     1.4  fun init_instantiation (tycos, vs, sort) thy =
     1.5    let
     1.6      val _ = if null tycos then error "At least one arity must be given" else ();
     1.7 -    val params = these_params thy sort;
     1.8 +    val params = these_params thy (filter (can (AxClass.get_info thy)) sort);
     1.9      fun get_param tyco (param, (_, (c, ty))) =
    1.10        if can (AxClass.param_of_inst thy) (c, tyco)
    1.11        then NONE else SOME ((c, tyco),
    1.12 @@ -513,7 +513,8 @@
    1.13        | SOME ts' => SOME (ts', ctxt);
    1.14      fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
    1.15       of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
    1.16 -         of SOME (_, ty') => if Type.raw_instance (ty', ty) then SOME (ty, ty') else NONE
    1.17 +         of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
    1.18 +              then SOME (ty, ty') else NONE
    1.19            | NONE => NONE)
    1.20        | NONE => NONE;
    1.21    in
    1.22 @@ -523,8 +524,7 @@
    1.23      |> fold (Variable.declare_typ o TFree) vs
    1.24      |> fold (Variable.declare_names o Free o snd) inst_params
    1.25      |> (Overloading.map_improvable_syntax o apfst)
    1.26 -         (fn ((_, _), ((_, subst), unchecks)) =>
    1.27 -            ((primary_constraints, []), (((improve, K NONE), false), [])))
    1.28 +         (K ((primary_constraints, []), (((improve, K NONE), false), [])))
    1.29      |> Overloading.add_improvable_syntax
    1.30      |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
    1.31      |> synchronize_inst_syntax