# HG changeset patch
# User clasohm
# Date 795268323 -3600
# Node ID 35c2e5e114c416613667fa0487f9e9989d2844e4
# Parent  f2c225386348557020b7f754762e7b68f40444ef
removed print_msg parameter of infer_types

diff -r f2c225386348 -r 35c2e5e114c4 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Mar 15 11:25:24 1995 +0100
+++ b/src/Pure/sign.ML	Wed Mar 15 12:52:03 1995 +0100
@@ -39,7 +39,7 @@
     val certify_term: sg -> term -> term * typ * int
     val read_typ: sg * (indexname -> sort option) -> string -> typ
     val infer_types: sg -> (indexname -> typ option) ->
-      (indexname -> sort option) -> string list -> bool -> bool
+      (indexname -> sort option) -> string list -> bool
       -> term list * typ -> int * term * (indexname * typ) list
     val add_classes: (class * class list) list -> sg -> sg
     val add_classrel: (class * class) list -> sg -> sg
@@ -252,7 +252,7 @@
 
 (** infer_types **)         (*exception ERROR*)
 
-fun infer_types sg types sorts used freeze print_msg (ts, T) =
+fun infer_types sg types sorts used freeze (ts, T) =
   let
     val Sg {tsig, ...} = sg;
     val show_typ = string_of_typ sg;
diff -r f2c225386348 -r 35c2e5e114c4 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Mar 15 11:25:24 1995 +0100
+++ b/src/Pure/thm.ML	Wed Mar 15 12:52:03 1995 +0100
@@ -199,7 +199,7 @@
       handle TYPE (msg, _, _) => error msg;
     val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a;
     val (_, t', tye) =
-          Sign.infer_types sign types sorts used freeze true (ts, T');
+          Sign.infer_types sign types sorts used freeze (ts, T');
     val ct = cterm_of sign t'
       handle TERM (msg, _) => error msg;
   in (ct, tye) end;
@@ -372,7 +372,7 @@
     handle ERROR => err_in_axm name;
 
 fun inferT_axm sg (name, pre_tm) =
-  let val t = #2(Sign.infer_types sg (K None) (K None) [] true true
+  let val t = #2(Sign.infer_types sg (K None) (K None) [] true
                                      ([pre_tm], propT))
   in  (name, no_vars t) end
   handle ERROR => err_in_axm name;