diff -r fafcc54e531d -r 646bfe5905b3 UnusedQuotMain.thy --- 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"} *}