1.1 --- a/src/Pure/Isar/code.ML	Thu Nov 04 17:27:37 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Nov 04 17:27:38 2010 +0100
     1.3 @@ -124,11 +124,23 @@
     1.4   of SOME c_ty => c_ty
     1.5    | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
     1.6  
     1.7 -fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy;
     1.8 +fun check_unoverload thy (c, ty) =
     1.9 +  let
    1.10 +    val c' = AxClass.unoverload_const thy (c, ty);
    1.11 +    val ty_decl = Sign.the_const_type thy c';
    1.12 +  in if Sign.typ_equiv thy
    1.13 +      (Type.strip_sorts ty_decl, Type.strip_sorts (Logic.varifyT_global ty)) then c'
    1.14 +    else error ("Type\n" ^ string_of_typ thy ty
    1.15 +      ^ "\nof constant " ^ quote c
    1.16 +      ^ "\nis too specific compared to declared type\n"
    1.17 +      ^ string_of_typ thy ty_decl)
    1.18 +  end; 
    1.19 +
    1.20 +fun check_const thy = check_unoverload thy o check_bare_const thy;
    1.21  
    1.22  fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
    1.23  
    1.24 -fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
    1.25 +fun read_const thy = check_unoverload thy o read_bare_const thy;
    1.26  
    1.27  
    1.28  (** data store **)
    1.29 @@ -471,7 +483,7 @@
    1.30    in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then ()
    1.31      else bad_thm ("Type\n" ^ string_of_typ thy ty
    1.32        ^ "\nof constant " ^ quote c
    1.33 -      ^ "\nis incompatible with declared type\n"
    1.34 +      ^ "\nis too specific compared to declared type\n"
    1.35        ^ string_of_typ thy ty_decl)
    1.36    end; 
    1.37  

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