--- a/FSet.thy	Tue Nov 10 17:43:05 2009 +0100
+++ b/FSet.thy	Wed Nov 11 10:22:47 2009 +0100
@@ -386,7 +386,7 @@
   apply (atomize(full))
   apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
   done*)
-ML {* val t_r = Toplevel.program (fn () => regularize t_a rty rel rel_eqv rel_refl @{context}) *}
+ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 ML {*
   val rt = build_repabs_term @{context} t_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
@@ -397,10 +397,8 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 
 done
-ML {* val t_t =
-  Toplevel.program (fn () =>
-  repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms
-  )
+ML {*
+val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms
 *}
 
 ML {* val abs = findabs rty (prop_of (t_a)) *}