
diff -r 7ef153ded7e2 -r 211229d6c66f UnusedQuotMain.thy
--- a/UnusedQuotMain.thy	Thu Nov 26 20:32:33 2009 +0100
+++ b/UnusedQuotMain.thy	Thu Nov 26 20:32:56 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"} *}
 
 
 




