removed print_msg parameter of infer_types
authorclasohm
Wed Mar 15 12:52:03 1995 +0100 (1995-03-15)
changeset 95935c2e5e114c4
parent 958 f2c225386348
child 960 358a19a91d52
removed print_msg parameter of infer_types
src/Pure/sign.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/sign.ML	Wed Mar 15 11:25:24 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Mar 15 12:52:03 1995 +0100
     1.3 @@ -39,7 +39,7 @@
     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) -> string list -> bool -> bool
     1.8 +      (indexname -> sort option) -> string list -> bool
     1.9        -> term list * typ -> int * term * (indexname * typ) list
    1.10      val add_classes: (class * class list) list -> sg -> sg
    1.11      val add_classrel: (class * class) list -> sg -> sg
    1.12 @@ -252,7 +252,7 @@
    1.13  
    1.14  (** infer_types **)         (*exception ERROR*)
    1.15  
    1.16 -fun infer_types sg types sorts used freeze print_msg (ts, T) =
    1.17 +fun infer_types sg types sorts used freeze (ts, T) =
    1.18    let
    1.19      val Sg {tsig, ...} = sg;
    1.20      val show_typ = string_of_typ sg;
     2.1 --- a/src/Pure/thm.ML	Wed Mar 15 11:25:24 1995 +0100
     2.2 +++ b/src/Pure/thm.ML	Wed Mar 15 12:52:03 1995 +0100
     2.3 @@ -199,7 +199,7 @@
     2.4        handle TYPE (msg, _, _) => error msg;
     2.5      val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
     2.6      val (_, t', tye) =
     2.7 -          Sign.infer_types sign types sorts used freeze true (ts, T');
     2.8 +          Sign.infer_types sign types sorts used freeze (ts, T');
     2.9      val ct = cterm_of sign t'
    2.10        handle TERM (msg, _) => error msg;
    2.11    in (ct, tye) end;
    2.12 @@ -372,7 +372,7 @@
    2.13      handle ERROR => err_in_axm name;
    2.14  
    2.15  fun inferT_axm sg (name, pre_tm) =
    2.16 -  let val t = #2(Sign.infer_types sg (K None) (K None) [] true true
    2.17 +  let val t = #2(Sign.infer_types sg (K None) (K None) [] true
    2.18                                       ([pre_tm], propT))
    2.19    in  (name, no_vars t) end
    2.20    handle ERROR => err_in_axm name;