--- a/IntEx.thy	Mon Nov 30 10:16:10 2009 +0100
+++ b/IntEx.thy	Mon Nov 30 11:53:20 2009 +0100
@@ -134,7 +134,7 @@
 
 ML {* val qty = @{typ "my_int"} *}
 ML {* val ty_name = "my_int" *}
-ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *}
+ML {* val rsp_thms = @{thms ho_plus_rsp} *}
 ML {* val defs = @{thms PLUS_def} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}