certify_term: tuned monomorphic consts;
authorwenzelm
Fri Oct 28 22:28:00 2005 +0200 (2005-10-28)
changeset 180323295e9982a5b
parent 18031 b17e25a7d820
child 18033 ab8803126f84
certify_term: tuned monomorphic consts;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri Oct 28 22:27:59 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Oct 28 22:28:00 2005 +0200
     1.3 @@ -295,7 +295,8 @@
     1.4    (case const_constraint thy c of SOME T => T
     1.5    | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
     1.6  
     1.7 -val const_type = Option.map (#1 o #1) oo (Symtab.lookup o #2 o #1 o #consts o rep_sg);
     1.8 +val lookup_const = Symtab.lookup o #2 o #1 o #consts o rep_sg;
     1.9 +val const_type = Option.map (#1 o #1) oo lookup_const;
    1.10  
    1.11  fun the_const_type thy c =
    1.12    (case const_type thy c of SOME T => T
    1.13 @@ -452,10 +453,10 @@
    1.14      fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
    1.15        | check_atoms (Abs (_, _, t)) = check_atoms t
    1.16        | check_atoms (Const (a, T)) =
    1.17 -          (case const_type thy a of
    1.18 +          (case lookup_const thy a of
    1.19              NONE => err ("Undeclared constant " ^ show_const a T)
    1.20 -          | SOME U =>
    1.21 -              if typ_instance thy (T, U) then ()
    1.22 +          | SOME ((U, mono), _) =>
    1.23 +              if mono andalso T = U orelse typ_instance thy (T, U) then ()
    1.24                else err ("Illegal type for constant " ^ show_const a T))
    1.25        | check_atoms (Var ((x, i), _)) =
    1.26            if i < 0 then err ("Malformed variable: " ^ quote x) else ()