removed constant _constrain from Pure sig;
authorwenzelm
Tue, 23 Aug 1994 19:31:05 +0200
changeset 573 2fa5ef27bd0a
parent 572 13c30ac40f8f
child 574 810da101bad2
removed constant _constrain from Pure sig;
src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Aug 22 11:27:23 1994 +0200
+++ b/src/Pure/sign.ML	Tue Aug 23 19:31:05 1994 +0200
@@ -6,7 +6,6 @@
 
 TODO:
   clean
-  pure sign: elim Syntax.constrainC
 *)
 
 signature SIGN =
@@ -523,8 +522,7 @@
     ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0)),
-    ("TYPE", "'a itself", NoSyn)(*,(* FIXME *)
-    (Syntax.constrainC, "'a::{} => 'a", NoSyn)*)]
+    ("TYPE", "'a itself", NoSyn)]
   |> add_name "Pure";