src/Pure/sign.ML
changeset 171 ab0f93a291b5
parent 169 1b2765146aab
child 197 7c7179e687b2
--- a/src/Pure/sign.ML	Tue Nov 30 10:55:43 1993 +0100
+++ b/src/Pure/sign.ML	Tue Nov 30 11:04:07 1993 +0100
@@ -132,12 +132,6 @@
     (*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
@@ -164,7 +158,6 @@
 
     val const_decs' =
       map (read_consts tsig' syn') (Syntax.constants sext @ const_decs);
-                    (* FIXME ^^^^ should be syn *)
   in
     Sg {
       tsig = tsig',
@@ -191,7 +184,7 @@
   (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);