src/Pure/sign.ML

       in typ_subst_TVars tye T end;
 
     (*read and check the type mentioned in a const declaration; zero type var
       indices because type inference requires it*)
 
-    (* FIXME bug / feature: varifyT'ed TFrees may clash with user specified
-      TVars e.g. foo :: "'a => ?'a" *)
-    (* FIXME if user supplied TVars were disallowed, zero_tvar_indices would
-      become obsolete *)
-    (* FIXME disallow "" as const name *)
-
     fun read_consts tsg sy (cs, s) =
       let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
       in
         (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of
           [] => (cs, ty)

 
     val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
 
     val const_decs' =
       map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
-                    (* FIXME ^^^^ should be syn *)
   in
     Sg {
       tsig = tsig',
       const_tab = Symtab.st_of_declist (const_decs', const_tab)
         handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),

  [(["fun"], 2),
   (["prop"], 0),
   (Syntax.syntax_types, 0)],
  [(["fun"],  ([["logic"], ["logic"]], "logic")),
   (["prop"], ([], "logic"))],
- [([Syntax.constrainC], "'a::logic => 'a")],  (* FIXME replace logic by {} (?) *)
+ [([Syntax.constrainC], "'a::logic => 'a")],
  Some Syntax.pure_sext);
 
 
 
 (** The Merge operation **)