--- a/Myhill.thy	Wed Jan 26 14:13:18 2011 +0000
+++ b/Myhill.thy	Wed Jan 26 22:23:56 2011 +0000
@@ -1,5 +1,5 @@
 theory Myhill
-  imports Main List_Prefix Prefix_subtract
+  imports Main List_Prefix Prefix_subtract Prelude
 begin
 
 (*
@@ -192,7 +192,7 @@
   *}
 lemma folds_alt_simp [simp]:
   "finite rs \<Longrightarrow> L (folds ALT NULL rs) = \<Union> (L ` rs)"
-apply (rule set_ext, simp add:folds_def)
+apply (rule set_eq_intro, simp add:folds_def)
 apply (rule someI2_ex, erule finite_imp_fold_graph)
 by (erule fold_graph.induct, auto)