--- a/UnusedQuotMain.thy	Thu Nov 26 19:51:31 2009 +0100
+++ b/UnusedQuotMain.thy	Thu Nov 26 20:18:36 2009 +0100
@@ -484,7 +484,7 @@
 
 
 ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
-ML {* atomize_goal @{theory} @{term "x = xa ⟹ a # x = a # xa"} *}
+ML {* atomize_goal @{theory} @{term "x = xa ? a # x = a # xa"} *}