--- a/FSet.thy	Mon Nov 23 14:05:02 2009 +0100
+++ b/FSet.thy	Mon Nov 23 14:16:41 2009 +0100
@@ -433,13 +433,9 @@
 ML {* ObjectLogic.rulify t_s *}
 
 ML {* val gl = @{term "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"} *}
-ML {* val vars = map Free (Term.add_frees gl []) *}
-ML {* fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm *}
-ML {* val gla = fold lambda_all vars gl *}
-ML {* val glf = Type.legacy_freeze gla *}
-ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
+ML {* val gla = atomize_goal @{theory} gl *}
 
-prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) (term_of glac) *}
+prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) gla *}
 
 ML_prf {*  fun tac ctxt = FIRST' [
       rtac rel_refl,
@@ -461,7 +457,7 @@
 
 ML {* val t_r = @{thm t_r} OF [t_a] *}
 
-ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, term_of glac) *}
+ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, gla) *}
 ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *}
 prove t_t: {* term_of si *}
 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}

--- a/QuotMain.thy	Mon Nov 23 14:05:02 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 14:16:41 2009 +0100
@@ -1206,6 +1206,20 @@
 (******************************************)
 
 ML {*
+fun atomize_goal thy gl =
+  let
+    val vars = map Free (Term.add_frees gl []);
+    fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm;
+    val gla = fold lambda_all vars gl
+    val glf = Type.legacy_freeze gla
+    val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf))
+  in
+    term_of glac
+  end
+*}
+
+
+ML {*
 (* builds the relation for respects *)
  
 fun mk_resp_arg lthy (rty, qty) =