# HG changeset patch
# User haftmann
# Date 1207781198 -7200
# Node ID 07d7d0a6d5fd2af318c1cc85bb3438a557661424
# Parent  855893d4d75f335f8067ee6bf2cf752829692af4
check validity of class target improvement

diff -r 855893d4d75f -r 07d7d0a6d5fd src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Apr 09 21:49:37 2008 +0200
+++ b/src/Pure/Isar/class.ML	Thu Apr 10 00:46:38 2008 +0200
@@ -411,6 +411,7 @@
 fun synchronize_class_syntax sups base_sort ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
+    val algebra = Sign.classes_of thy;
     val operations = these_operations thy sups;
     fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
     val primary_constraints =
@@ -423,10 +424,11 @@
     fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
      of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
          of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
-             of SOME (_, ty' as TVar (tvar as (vi, _))) =>
+             of SOME (_, ty' as TVar (tvar as (vi, sort))) =>
                   if TypeInfer.is_param vi
-                    then SOME (ty', TFree (Name.aT, base_sort))
-                    else NONE
+                    andalso Sorts.sort_le algebra (base_sort, sort)
+                      then SOME (ty', TFree (Name.aT, base_sort))
+                      else NONE
               | _ => NONE)
           | NONE => NONE)
       | NONE => NONE)