--- a/IntEx.thy	Thu Nov 05 09:38:34 2009 +0100
+++ b/IntEx.thy	Thu Nov 05 09:55:21 2009 +0100
@@ -158,7 +158,8 @@
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val t_a = atomize_thm @{thm ho_tst} *}
 
-(*prove t_r: {* build_regularize_goal t_a rty rel @{context} *}
+(*
+prove t_r: {* build_regularize_goal t_a rty rel @{context} *}
 ML_prf {*   fun tac ctxt =
       (ObjectLogic.full_atomize_tac) THEN'
      REPEAT_ALL_NEW (FIRST' [
@@ -183,6 +184,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) ===>