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