--- a/FSet.thy	Fri Oct 30 15:52:47 2009 +0100
+++ b/FSet.thy	Fri Oct 30 16:24:07 2009 +0100
@@ -169,9 +169,9 @@
 
 (* FIXME: does not work yet for all types*)
 quotient_def (for "'a fset")
-  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
+  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
-  "fmap \<equiv> (map::('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list)"
+  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
 term map
 term fmap
@@ -309,6 +309,7 @@
 lemma eq_r: "a = b \<Longrightarrow> a \<approx> b"
 by (simp add: list_eq_refl)
 
+(* ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *} *)
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
@@ -319,16 +320,18 @@
 
 thm fold1.simps(2)
 thm list.recs(2)
+thm list.cases
+
 
 ML {* val ind_r_a = atomize_thm @{thm list.induct} *}
-(*  prove {* build_regularize_goal ind_r_a rty rel @{context} *}
+(*prove {* build_regularize_goal ind_r_a rty rel @{context}  *}
   ML_prf {*  fun tac ctxt =
        (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW
          (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN'
          (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); *}
-  apply (tactic {* tac @{context} 1 *}) *)
+  apply (tactic {* tac @{context} 1 *})*)
 ML {* val ind_r_r = regularize ind_r_a rty rel rel_eqv @{context} *}
 ML {*
   val rt = build_repabs_term @{context} ind_r_r consts rty qty