--- a/IntEx.thy	Mon Nov 30 15:40:22 2009 +0100
+++ b/IntEx.thy	Tue Dec 01 12:16:45 2009 +0100
@@ -150,9 +150,7 @@
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
-apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 apply(simp add: id_def)
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -194,9 +192,7 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(simp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
-apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done
 
 lemma ho_tst: "foldl my_plus x [] = x"
@@ -217,10 +213,8 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 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 *})
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 sorry
 
 (*
@@ -233,9 +227,7 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(simp)
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) 
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
-apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done