# HG changeset patch
# User wenzelm
# Date 780598545 -3600
# Node ID f787eb061618bd8e0036f68e60f24476256e6289
# Parent  a0342b27b38e523a0bdd3052de27254ccbe7906f
exported pretty_sort;
various minor internal changes;

diff -r a0342b27b38e -r f787eb061618 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Sep 26 17:36:10 1994 +0100
+++ b/src/Pure/sign.ML	Mon Sep 26 17:55:45 1994 +0100
@@ -3,9 +3,6 @@
     Author:     Lawrence C Paulson and Markus Wenzel
 
 The abstract type "sg" of signatures.
-
-TODO:
-  clean
 *)
 
 signature SIGN =
@@ -33,6 +30,7 @@
     val pprint_sg: sg -> pprint_args -> unit
     val pretty_term: sg -> term -> Pretty.T
     val pretty_typ: sg -> typ -> Pretty.T
+    val pretty_sort: sort -> Pretty.T
     val string_of_term: sg -> term -> string
     val string_of_typ: sg -> typ -> string
     val pprint_term: sg -> term -> pprint_args -> unit
@@ -111,13 +109,16 @@
   Symtab.lookup (const_tab, c);
 
 
-(* classes *)
+(* classes and sorts *)
 
 val classes = #classes o Type.rep_tsig o tsig_of;
 
 val subsort = Type.subsort o tsig_of;
 val norm_sort = Type.norm_sort o tsig_of;
 
+fun pretty_sort [c] = Pretty.str c
+  | pretty_sort cs = Pretty.str_list "{" "}" cs;
+
 
 
 (** print signature **)
@@ -128,9 +129,6 @@
   let
     fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
 
-    fun pretty_sort [cl] = Pretty.str cl
-      | pretty_sort cls = Pretty.str_list "{" "}" cls;
-
     fun pretty_subclass (cl, cls) = Pretty.block
       [Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls];
 
@@ -140,7 +138,7 @@
     fun pretty_arg (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
 
     fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block
-      [prt_typ syn (Type (ty, map (fn v => TVar (v, [])) vs)),
+      [prt_typ syn (Type (ty, map (fn v => TVar ((v, 0), [])) vs)),
         Pretty.str " =", Pretty.brk 1, prt_typ syn rhs];
 
     fun pretty_arity ty (cl, []) = Pretty.block
@@ -264,32 +262,7 @@
 
 
 
-(** extend signature **)    (*exception ERROR*)
-
-(* FIXME -> type.ML *)
-
-(* FIXME replace? *)
-fun varify_typ (Type (t, tys)) = Type (t, map varify_typ tys)
-  | varify_typ (TFree (a, s)) = TVar ((a, 0), s)
-  | varify_typ (ty as TVar _) =
-      raise_type "Illegal schematic type variable" [ty] [];
-
-
-(* fake newstyle interfaces *) (* FIXME -> type.ML *)
-
-fun ext_tsig_classes tsig classes =
-  extend_tsig tsig (classes, [], [], []);
-
-(* FIXME varify_typ, rem_sorts; norm_typ (?) *)
-fun ext_tsig_abbrs tsig abbrs = Type.ext_tsig_abbrs tsig
-  (map (fn (t, vs, rhs) => (t, (map (rpair 0) vs, varifyT rhs))) abbrs);
-
-fun ext_tsig_arities tsig arities = extend_tsig tsig
-  ([], [], [], flat (map (fn (t, ss, cs) => map (fn c => ([t], (ss, c))) cs) arities));
-
-
-
-(** extension functions **)  (*exception ERROR*)
+(** signature extension functions **)  (*exception ERROR*)
 
 fun decls_of name_of mfixs =
   map (fn (x, y, mx) => (name_of x mx, y)) mfixs;
@@ -354,15 +327,9 @@
   (c, read_raw_typ syn tsig (K None) ty_src, mx)
     handle ERROR => err_in_const (Syntax.const_name c mx);
 
-(* FIXME move *)
-fun no_tvars ty =
-  if null (typ_tvars ty) then ty
-  else raise_type "Illegal schematic type variable(s)" [ty] [];
-
 fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   let
-    (* FIXME clean *)
-    fun prep_const (c, ty, mx) = (c, varify_typ (cert_typ tsig (no_tvars ty)), mx)
+    fun prep_const (c, ty, mx) = (c, varifyT (cert_typ tsig (no_tvars ty)), mx)
       handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
 
     val consts = map (prep_const o rd_const syn tsig) raw_consts;
@@ -461,7 +428,7 @@
 
 
 
-(** merge signatures **)    (*exception TERM*)
+(** merge signatures **)    (*exception TERM*) (*exception ERROR (* FIXME *)*)
 
 fun merge (sg1, sg2) =
   if subsig (sg2, sg1) then sg1