# HG changeset patch
# User wenzelm
# Date 778849838 -7200
# Node ID 550292083e66a5eefcd17b822ea96fb9359c526a
# Parent  8f1f1fab70ad4fb357694db5ec4d6eebac6de0d6
minor internal changes;

diff -r 8f1f1fab70ad -r 550292083e66 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Sep 06 13:09:58 1994 +0200
+++ b/src/Pure/sign.ML	Tue Sep 06 13:10:38 1994 +0200
@@ -26,8 +26,8 @@
     val is_draft: sg -> bool
     val const_type: sg -> string -> typ option
     val classes: sg -> class list
-    val subsort: sg -> sort * sort -> bool      (* FIXME move? *)
-    val norm_sort: sg -> sort -> sort           (* FIXME move? *)
+    val subsort: sg -> sort * sort -> bool
+    val norm_sort: sg -> sort -> sort
     val print_sg: sg -> unit
     val pretty_sg: sg -> Pretty.T
     val pprint_sg: sg -> pprint_args -> unit
@@ -243,7 +243,7 @@
 
 
 
-(** infer_types **)         (*exception ERROR*)   (* FIXME check *)
+(** infer_types **)         (*exception ERROR*)
 
 fun infer_types sg types sorts (t, T) =
   let
@@ -280,9 +280,6 @@
 fun ext_tsig_classes tsig classes =
   extend_tsig tsig (classes, [], [], []);
 
-fun ext_tsig_types tsig types =
-  extend_tsig tsig ([], [], map (fn (t, n) => ([t], n)) types, []);
-
 (* 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);