--- 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;
--- 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;