src/Pure/sign.ML
changeset 1216 a2f2360ce1c8
parent 1214 3f3888213ceb
child 1239 2c0d94151e74
     1.1 --- a/src/Pure/sign.ML	Tue Aug 01 17:17:49 1995 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Aug 01 17:19:17 1995 +0200
     1.3 @@ -25,6 +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 print_sg: sg -> unit
     1.9      val pretty_sg: sg -> Pretty.T
    1.10      val pprint_sg: sg -> pprint_args -> unit
    1.11 @@ -62,7 +63,6 @@
    1.12      val add_name: string -> sg -> sg
    1.13      val make_draft: sg -> sg
    1.14      val merge: sg * sg -> sg
    1.15 -    val nonempty_sort: sg * sort list * sort -> bool
    1.16      val proto_pure: sg
    1.17      val pure: sg
    1.18      val cpure: sg
    1.19 @@ -120,6 +120,7 @@
    1.20  
    1.21  val subsort = Type.subsort o tsig_of;
    1.22  val norm_sort = Type.norm_sort o tsig_of;
    1.23 +val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.24  
    1.25  fun pretty_sort [c] = Pretty.str c
    1.26    | pretty_sort cs = Pretty.str_list "{" "}" cs;
    1.27 @@ -135,7 +136,8 @@
    1.28      fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
    1.29  
    1.30      fun pretty_subclass (cl, cls) = Pretty.block
    1.31 -      [Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls];
    1.32 +      (Pretty.str (cl ^ " <") :: Pretty.brk 1 ::
    1.33 +        Pretty.commas (map Pretty.str cls));
    1.34  
    1.35      fun pretty_default cls = Pretty.block
    1.36        [Pretty.str "default:", Pretty.brk 1, pretty_sort cls];
    1.37 @@ -552,11 +554,4 @@
    1.38    |> add_syntax Syntax.pure_applC_syntax
    1.39    |> add_name "CPure";
    1.40  
    1.41 -(**
    1.42 -Emptiness-test for sorts: does there exist a type of sort 'sort' whose
    1.43 -vars have sorts contained in 'sorts'?
    1.44 -Trivial approximation at the moment.
    1.45 -**)
    1.46 -fun nonempty_sort(_,sorts,sort) = exists (fn s => sort subset s) sorts;
    1.47 -
    1.48  end;