Add failing test-cases for github issue #503

This bug has the free-bound status of the restricted variable
contaminate the free/bound status of variables within the restriction.
The printer is also too keen to see restrictions as identical when
they are not because the freeness of variables within the restrictions
are different.

src/1/selftest.sml

@@ -406,7 +406,7 @@ fun tpp (s,expected) = let
   val res = ppstring pp_term t
 in
   if res = expected then OK()
-  else (print "FAILED\n"; Process.exit Process.failure)
+  else die ("FAILED\n  Expected >" ^ expected ^ "<; got "^res)
 end
 
 fun bound s = "\^[[0;32m" ^ s ^ "\^[[0m"
@@ -425,7 +425,12 @@ val _ = app tpp [
    concat ["let ",bx, " = ", fp, " in ", bx, " /\\ ", fy]),
   ("let f x = x /\\ p in f x /\\ y",
    concat ["let ",bound "f", " ", bx, " = ", bx, " /\\ ", fp, " in ",
-           bound "f", " ", fx, " /\\ ", fy])
+           bound "f", " ", fx, " /\\ ", fy]),
+  ("!(x:'a)::p (x:'a). q x",
+   concat ["!",bx,"::",fp, " ", fx,". ",free "q"," ",bx]),
+  ("RES_FORALL (p (x:'a)) (\\x. RES_FORALL (p (x:'a)) (\\y. q x y))",
+   concat ["!(",bx,"::",fp," ",fx,") (",bound "y","::",fp," ",bx,"). ",
+           free "q", " ", bx, " ", bound "y"])
 ]
 
 open testutils