Code.check_const etc.: reject too specific types

--- a/src/Pure/Isar/code.ML	Thu Nov 04 17:27:37 2010 +0100
+++ b/src/Pure/Isar/code.ML	Thu Nov 04 17:27:38 2010 +0100
@@ -124,11 +124,23 @@
  of SOME c_ty => c_ty
   | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
 
-fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
+fun check_unoverload thy (c, ty) =
+  let
+    val c' = AxClass.unoverload_const thy (c, ty);
+    val ty_decl = Sign.the_const_type thy c';
+  in if Sign.typ_equiv thy
+      (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty)) then c'
+    else error ("Type\n" ^ string_of_typ thy ty
+      ^ "\nof constant " ^ quote c
+      ^ "\nis too specific compared to declared type\n"
+      ^ string_of_typ thy ty_decl)
+  end; 
+
+fun check_const thy = check_unoverload thy o check_bare_const thy;
 
 fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
 
-fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
+fun read_const thy = check_unoverload thy o read_bare_const thy;
 
 
 (** data store **)
@@ -471,7 +483,7 @@
   in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then ()
     else bad_thm ("Type\n" ^ string_of_typ thy ty
       ^ "\nof constant " ^ quote c
-      ^ "\nis incompatible with declared type\n"
+      ^ "\nis too specific compared to declared type\n"
       ^ string_of_typ thy ty_decl)
   end; 
 

--- a/src/Tools/nbe.ML	Thu Nov 04 17:27:37 2010 +0100
+++ b/src/Tools/nbe.ML	Thu Nov 04 17:27:38 2010 +0100
@@ -64,7 +64,7 @@
     val lhs_rhs = case try Logic.dest_equals eqn
      of SOME lhs_rhs => lhs_rhs
       | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
-    val c_c' = case try (pairself (Code.check_const thy)) lhs_rhs
+    val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
      of SOME c_c' => c_c'
       | _ => error ("Not an equation with two constants: "
           ^ Syntax.string_of_term_global thy eqn);