--- 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)) *}

--- a/IntEx.thy	Tue Nov 10 17:43:05 2009 +0100
+++ b/IntEx.thy	Wed Nov 11 10:22:47 2009 +0100
@@ -223,7 +223,7 @@
 ML {* val aps = findaps rty (prop_of t_a); *}
 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 
-(*ML {* val t_t = Toplevel.program (fn () => repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms) *}*)
+(*ML {* val t_t = repabs @{context} @{thm t_r} consts rty qty quot rel_refl trans2 rsp_thms *}*)
 ML {* val (alls, exs) = findallex rty qty (prop_of t_a) *}
 ML {* val allthms = map (make_allex_prs_thm @{context} quot @{thm FORALL_PRS}) alls *}
 ML {* val t_a = MetaSimplifier.rewrite_rule (allthms) t_t *}

--- a/QuotTest.thy	Tue Nov 10 17:43:05 2009 +0100
+++ b/QuotTest.thy	Wed Nov 11 10:22:47 2009 +0100
@@ -98,9 +98,7 @@
 (* A test whether get_fun works properly
 consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
 local_setup {*
-  fn lthy => (Toplevel.program (fn () =>
-    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
-  )) |> snd
+    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |> snd
 *}
 *)