--- a/FSet.thy	Mon Nov 23 21:59:57 2009 +0100
+++ b/FSet.thy	Mon Nov 23 22:00:54 2009 +0100
@@ -328,21 +328,22 @@
 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_fset @{context} @{thm map_append} *}
-ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION x xa) = FUNION (fmap f x) (fmap f xa)"} *}
+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 *}
+
+ML {* lift_thm_g_fset @{context} @{thm map_append} gl *}
+
 
 ML {* lift_thm_fset @{context} @{thm list.induct} *}
 ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"} *}
 
 
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val rtrm = prop_of (atomize_thm @{thm append_assoc}) *}
-ML {* val qtrm = goal_a *}
-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 *}
-
-ML {* lift_thm_g_fset @{context} @{thm append_assoc} gl *}
-
 
 
 (*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*)