--- a/IntEx.thy	Sun Nov 29 02:51:42 2009 +0100
+++ b/IntEx.thy	Sun Nov 29 03:59:18 2009 +0100
@@ -128,9 +128,9 @@
   apply(auto)
   done
 
-lemma ho_plus_rsp:
-  "(intrel ===> intrel ===> intrel) my_plus my_plus"
-  by (simp)
+lemma ho_plus_rsp[quot_rsp]:
+  shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
+by (simp)
 
 ML {* val qty = @{typ "my_int"} *}
 ML {* val ty_name = "my_int" *}
@@ -140,10 +140,10 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 ML {* val consts = lookup_quot_consts defs *}
 
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
 
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
 
 
 lemma "PLUS a b = PLUS b a"
@@ -199,17 +199,19 @@
 apply simp
 done
 
-lemma map_prs: "map REP_my_int (map ABS_my_int x) = x"
+(* FIXME/TODO: is this a respectfulness theorem? Does not look like one. *)
+lemma map_prs: 
+  "map REP_my_int (map ABS_my_int x) = x"
 sorry
 
-lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
+lemma foldl_prs[quot_rsp]: 
+  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
 sorry
 
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(rule foldl_prs) 
 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) *}