src/Pure/sign.ML
changeset 959 35c2e5e114c4
parent 952 9e10962866b0
child 963 7a78fda77104
     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;