diff -r 329111e1c4ba -r f219011a5e3c FSet.thy
--- a/FSet.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/FSet.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -306,8 +306,12 @@
   apply (metis)
   done
 
+ML {* (atomize_thm @{thm list_induct_hol4}) *}
+
+ML {* regularise (prop_of (atomize_thm @{thm list_induct_hol4})) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
+
 prove list_induct_r: {*
-   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
+   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a list"} @{term "op \<approx>"} @{context} *}
   apply (simp only: equiv_res_forall[OF equiv_list_eq])
   thm RIGHT_RES_FORALL_REGULAR
   apply (rule RIGHT_RES_FORALL_REGULAR)