# HG changeset patch
# User haftmann
# Date 1234981112 -3600
# Node ID 9dbb046136d0aeb00d51a71784e8415c85b46d20
# Parent  7171f3f058b65bc52b783bb53b717bba0f7b65fa
more precise improvement in instantiation user space type system

diff -r 7171f3f058b6 -r 9dbb046136d0 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Feb 18 19:18:31 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Wed Feb 18 19:18:32 2009 +0100
@@ -493,7 +493,7 @@
 fun init_instantiation (tycos, vs, sort) thy =
   let
     val _ = if null tycos then error "At least one arity must be given" else ();
-    val params = these_params thy sort;
+    val params = these_params thy (filter (can (AxClass.get_info thy)) sort);
     fun get_param tyco (param, (_, (c, ty))) =
       if can (AxClass.param_of_inst thy) (c, tyco)
       then NONE else SOME ((c, tyco),
@@ -513,7 +513,8 @@
       | SOME ts' => SOME (ts', ctxt);
     fun improve (c, ty) = case AxClass.inst_tyco_of thy (c, ty)
      of SOME tyco => (case AList.lookup (op =) inst_params (c, tyco)
-         of SOME (_, ty') => if Type.raw_instance (ty', ty) then SOME (ty, ty') else NONE
+         of SOME (_, ty') => if Type.typ_instance (Sign.tsig_of thy) (ty', ty)
+              then SOME (ty, ty') else NONE
           | NONE => NONE)
       | NONE => NONE;
   in
@@ -523,8 +524,7 @@
     |> fold (Variable.declare_typ o TFree) vs
     |> fold (Variable.declare_names o Free o snd) inst_params
     |> (Overloading.map_improvable_syntax o apfst)
-         (fn ((_, _), ((_, subst), unchecks)) =>
-            ((primary_constraints, []), (((improve, K NONE), false), [])))
+         (K ((primary_constraints, []), (((improve, K NONE), false), [])))
     |> Overloading.add_improvable_syntax
     |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax