--- a/FSet.thy	Mon Nov 23 22:00:54 2009 +0100
+++ b/FSet.thy	Mon Nov 23 23:09:03 2009 +0100
@@ -311,29 +311,34 @@
 ML {* lift_thm_fset @{context} @{thm m1} *}
 ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"} *}
 ML {* lift_thm_fset @{context} @{thm m2} *}
+
 ML {* lift_thm_g_fset @{context} @{thm m2} @{term "IN x (INSERT y xa) = (x = y \<or> IN x xa)"} *}
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(4)} *}
 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(4)} @{term "INSERT a (INSERT a x) = INSERT a x"} *}
+
 ML {* lift_thm_fset @{context} @{thm list_eq.intros(5)} *}
 ML {* lift_thm_g_fset @{context} @{thm list_eq.intros(5)} @{term "x = xa \<Longrightarrow> INSERT a x = INSERT a xa"} *}
 ML {* lift_thm_fset @{context} @{thm card1_suc} *}
-ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \<Longrightarrow> \<exists>a b. \<not> IN a b \<and> x = INSERT a b"} *}
+ML {* lift_thm_g_fset @{context} @{thm card1_suc} @{term "CARD x = Suc n \<Longrightarrow> \<exists>a b. \<not> IN a b \<and> x = INSERT a b"} *} 
 ML {* lift_thm_fset @{context} @{thm not_mem_card1} *}
 ML {* lift_thm_g_fset @{context} @{thm not_mem_card1} @{term "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"} *}
 ML {* lift_thm_fset @{context} @{thm fold1.simps(2)} *}
 (* Doesn't work with 'a, 'b, but works with 'b, 'a *)
+
 ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) =
     (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}
 
 ML {* lift_thm_fset @{context} @{thm append_assoc} *}
-ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *}
+ML {* lift_thm_g_fset @{context} @{thm append_assoc} @{term "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)"} *} 
 ML {* lift_thm_fset @{context} @{thm map_append} *}
 ML {* val gl = @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *}
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val rtrm = prop_of (atomize_thm @{thm map_append}) *}
+
 ML {* val qtrm = atomize_goal @{theory} gl *}
 ML {* val a = (REGULARIZE_trm @{context} rtrm qtrm) *}
+
 ML {* val a = Syntax.check_term @{context} a *}
 ML {* val t_r = regularize_goal @{context} (atomize_thm @{thm append_assoc}) rel_eqv rel_refl goal_a *}