# 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 ()