# HG changeset patch
# User wenzelm
# Date 1130531280 -7200
# Node ID 3295e9982a5b57658c8bd37e1ec8ef5b9efe7437
# Parent  b17e25a7d8208f07e329d2e991f0ec32109a44b6
certify_term: tuned monomorphic consts;

diff -r b17e25a7d820 -r 3295e9982a5b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Oct 28 22:27:59 2005 +0200
+++ b/src/Pure/sign.ML	Fri Oct 28 22:28:00 2005 +0200
@@ -295,7 +295,8 @@
   (case const_constraint thy c of SOME T => T
   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
 
-val const_type = Option.map (#1 o #1) oo (Symtab.lookup o #2 o #1 o #consts o rep_sg);
+val lookup_const = Symtab.lookup o #2 o #1 o #consts o rep_sg;
+val const_type = Option.map (#1 o #1) oo lookup_const;
 
 fun the_const_type thy c =
   (case const_type thy c of SOME T => T
@@ -452,10 +453,10 @@
     fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
       | check_atoms (Abs (_, _, t)) = check_atoms t
       | check_atoms (Const (a, T)) =
-          (case const_type thy a of
+          (case lookup_const thy a of
             NONE => err ("Undeclared constant " ^ show_const a T)
-          | SOME U =>
-              if typ_instance thy (T, U) then ()
+          | SOME ((U, mono), _) =>
+              if mono andalso T = U orelse typ_instance thy (T, U) then ()
               else err ("Illegal type for constant " ^ show_const a T))
       | check_atoms (Var ((x, i), _)) =
           if i < 0 then err ("Malformed variable: " ^ quote x) else ()