--- a/IntEx.thy	Sun Nov 29 03:59:18 2009 +0100
+++ b/IntEx.thy	Sun Nov 29 08:48:06 2009 +0100
@@ -215,6 +215,8 @@
 apply(simp add: map_prs)
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm ho_tst})) (term_of qtm) *}
+apply(simp only: map_prs)
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
 sorry
 
 (*