src/Pure/sign.ML

     val subsig: sg * sg -> bool
     val eq_sg: sg * sg -> bool
     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
     val pretty_term: sg -> term -> Pretty.T
     val pretty_typ: sg -> typ -> Pretty.T

     | errs => raise_type (cat_lines errs) [] [norm_tm])
   end;
 
 
 
-(** infer_types **)         (*exception ERROR*)   (* FIXME check *)
+(** infer_types **)         (*exception ERROR*)
 
 fun infer_types sg types sorts (t, T) =
   let
     val Sg {tsig, ...} = sg;
     val show_typ = string_of_typ sg;

 
 (* fake newstyle interfaces *) (* FIXME -> type.ML *)
 
 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);