--- a/IntEx.thy	Mon Nov 23 14:32:11 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 14:40:53 2009 +0100
@@ -278,7 +278,7 @@
   val rt = build_repabs_term @{context} t_r consts rty qty
   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
 *}
-*)
+
 
 lemma foldl_rsp:
   "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===>
@@ -312,11 +312,12 @@
 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
 
 (*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 findallex
+ML {* val (alls, exs) = findallex @{context} 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 *}
 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *}
-ML {* val defs_sym = add_lower_defs @{context} defs *}
+ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *}
 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *}
 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
 ML {* ObjectLogic.rulify t_r *}