nonempty_sort: no longer var names as args;
authorwenzelm
Fri Sep 01 13:13:19 1995 +0200 (1995-09-01)
changeset 12392c0d94151e74
parent 1238 289c573327f0
child 1240 0901441a7ebf
nonempty_sort: no longer var names as args;
src/Pure/sign.ML
src/Pure/type.ML
     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) =
     2.1 --- a/src/Pure/type.ML	Fri Sep 01 13:11:09 1995 +0200
     2.2 +++ b/src/Pure/type.ML	Fri Sep 01 13:13:19 1995 +0200
     2.3 @@ -38,7 +38,7 @@
     2.4    val subsort: type_sig -> sort * sort -> bool
     2.5    val norm_sort: type_sig -> sort -> sort
     2.6    val rem_sorts: typ -> typ
     2.7 -  val nonempty_sort: type_sig -> (string * sort) list -> sort -> bool
     2.8 +  val nonempty_sort: type_sig -> sort list -> sort -> bool
     2.9    val cert_typ: type_sig -> typ -> typ
    2.10    val norm_typ: type_sig -> typ -> typ
    2.11    val freeze: term -> term
    2.12 @@ -406,7 +406,7 @@
    2.13  fun nonempty_sort _ _ [] = true
    2.14    | nonempty_sort (tsig as TySg {arities, ...}) hyps S =
    2.15        exists (exists (fn (c, ss) => [c] = S andalso null ss) o snd) arities
    2.16 -        orelse exists (fn (_, S') => subsort tsig (S', S)) hyps;
    2.17 +        orelse exists (fn S' => subsort tsig (S', S)) hyps;
    2.18  
    2.19  
    2.20