src/Pure/sign.ML
changeset 949 83c588d6fee9
parent 926 9d1348498c36
child 952 9e10962866b0
     1.1 --- a/src/Pure/sign.ML	Sat Mar 11 17:46:14 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Mon Mar 13 09:38:10 1995 +0100
     1.3 @@ -39,8 +39,8 @@
     1.4      val certify_term: sg -> term -> term * typ * int
     1.5      val read_typ: sg * (indexname -> sort option) -> string -> typ
     1.6      val infer_types: sg -> (indexname -> typ option) ->
     1.7 -      (indexname -> sort option) -> bool -> term list * typ ->
     1.8 -      int * term * (indexname * typ) list
     1.9 +      (indexname -> sort option) -> string list -> bool -> bool
    1.10 +      -> term list * typ -> int * term * (indexname * typ) list
    1.11      val add_classes: (class * class list) list -> sg -> sg
    1.12      val add_classrel: (class * class) list -> sg -> sg
    1.13      val add_defsort: sort -> sg -> sg
    1.14 @@ -252,7 +252,7 @@
    1.15  
    1.16  (** infer_types **)         (*exception ERROR*)
    1.17  
    1.18 -fun infer_types sg types sorts print_msg (ts, T) =
    1.19 +fun infer_types sg types sorts used freeze print_msg (ts, T) =
    1.20    let
    1.21      val Sg {tsig, ...} = sg;
    1.22      val show_typ = string_of_typ sg;
    1.23 @@ -268,16 +268,16 @@
    1.24  	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n";
    1.25  
    1.26      val T' = certify_typ sg T
    1.27 -      handle TYPE arg => error (exn_type_msg arg);
    1.28 +             handle TYPE arg => error (exn_type_msg arg);
    1.29  
    1.30      val ct = const_type sg;
    1.31  
    1.32      fun process_terms (t::ts) (idx, infrd_t, tye) msg n =
    1.33 -         let fun mk_some (x, y) = (Some x, Some y);
    1.34 -
    1.35 -             val ((infrd_t', tye'), msg') = 
    1.36 -              (mk_some (Type.infer_types (tsig, ct, types, sorts, T', t)), msg)
    1.37 -              handle TYPE arg => ((None, None), exn_type_msg arg)
    1.38 +         let val (infrd_t', tye', msg') = 
    1.39 +              let val (T,tye) =
    1.40 +                    Type.infer_types(tsig,ct,types,sorts,used,freeze,T',t)
    1.41 +              in (Some T, Some tye, msg) end
    1.42 +              handle TYPE arg => (None, None, exn_type_msg arg)
    1.43  
    1.44               val old_show_brackets = !show_brackets;
    1.45  
    1.46 @@ -291,8 +291,8 @@
    1.47                  (show_term (the infrd_t)) else msg') ^ "\n" ^ 
    1.48                  (show_term (the infrd_t')) ^ "\n";
    1.49  
    1.50 -             val _ = (show_brackets := old_show_brackets);
    1.51 -         in if is_none infrd_t' then
    1.52 +         in show_brackets := old_show_brackets;
    1.53 +            if is_none infrd_t' then
    1.54                process_terms ts (idx, infrd_t, tye) msg'' (n+1)
    1.55              else
    1.56                process_terms ts (Some n, infrd_t', tye') msg'' (n+1)