src/Pure/sign.ML
changeset 1239 2c0d94151e74
parent 1216 a2f2360ce1c8
child 1241 bfc93c86f0a1
     1.1 --- a/src/Pure/sign.ML	Fri Sep 01 13:11:09 1995 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Sep 01 13:13:19 1995 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4      val classes: sg -> class list
     1.5      val subsort: sg -> sort * sort -> bool
     1.6      val norm_sort: sg -> sort -> sort
     1.7 -    val nonempty_sort: sg -> (string * sort) list -> sort -> bool
     1.8 +    val nonempty_sort: sg -> sort list -> sort -> bool
     1.9      val print_sg: sg -> unit
    1.10      val pretty_sg: sg -> Pretty.T
    1.11      val pprint_sg: sg -> pprint_args -> unit
    1.12 @@ -193,7 +193,7 @@
    1.13  
    1.14  fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
    1.15  
    1.16 -fun string_of_term (Sg {syn, stamps, ...}) = 
    1.17 +fun string_of_term (Sg {syn, stamps, ...}) =
    1.18    let val curried = "CPure" mem (map ! stamps);
    1.19    in Syntax.string_of_term curried syn end;
    1.20  
    1.21 @@ -266,7 +266,7 @@
    1.22  
    1.23      fun term_err [] = ""
    1.24        | term_err [t] = "\nInvolving this term:\n" ^ show_term t
    1.25 -      | term_err ts = 
    1.26 +      | term_err ts =
    1.27            "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
    1.28  
    1.29      fun exn_type_msg (msg, Ts, ts) =