From 201b5216af7a8ec183a262e8fbedd7514e774fd4 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 2 Apr 2004 18:22:20 +0000
Subject: Add extra term test -- shows up current bug

---
 etc/isar/XSymbolTests.thy | 1 +
 1 file changed, 1 insertion(+)

diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy
index 3b5ccf00..ebafcf8b 100644
--- a/etc/isar/XSymbolTests.thy
+++ b/etc/isar/XSymbolTests.thy
@@ -17,6 +17,7 @@ consts silly:: "'a => 'a => 'a" ("_\<^sup>_" [1000,1000] 1000)
 consts k:: 'a
 
 term "a\<^sup>b" (* b should be a blue variable *)
+term "\<forall> x. a\<^sup>x" (* x should be a green bound variable *)
 term "a\<^sup>k" (* k should be a black constant *)
 
 
-- 
cgit v1.2.3