removed constant _constrain from Pure sig;
authorwenzelm
Tue Aug 23 19:31:05 1994 +0200 (1994-08-23)
changeset 5732fa5ef27bd0a
parent 572 13c30ac40f8f
child 574 810da101bad2
removed constant _constrain from Pure sig;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Mon Aug 22 11:27:23 1994 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Aug 23 19:31:05 1994 +0200
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  TODO:
     1.6    clean
     1.7 -  pure sign: elim Syntax.constrainC
     1.8  *)
     1.9  
    1.10  signature SIGN =
    1.11 @@ -523,8 +522,7 @@
    1.12      ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
    1.13      ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
    1.14      ("all", "('a => prop) => prop", Binder ("!!", 0)),
    1.15 -    ("TYPE", "'a itself", NoSyn)(*,(* FIXME *)
    1.16 -    (Syntax.constrainC, "'a::{} => 'a", NoSyn)*)]
    1.17 +    ("TYPE", "'a itself", NoSyn)]
    1.18    |> add_name "Pure";
    1.19  
    1.20