--- a/QuotMain.thy	Fri Nov 27 02:55:56 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 02:58:28 2009 +0100
@@ -725,9 +725,6 @@
   handle _ => no_tac)
 *}
 
-ML {*
-fun CHANGED' tac = (fn i => CHANGED (tac i))
-*}
 
 ML {*
 fun quotient_tac quot_thm =
@@ -736,7 +733,7 @@
     rtac quot_thm,
     rtac @{thm IDENTITY_QUOTIENT},
     (* For functional identity quotients, (op = ---> op =) *)
-    CHANGED' (simp_tac (HOL_ss addsimps @{thms id_simps}))
+    CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))
   ])
 *}
 
@@ -833,7 +830,7 @@
     atac,
     SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
     WEAK_LAMBDA_RES_TAC ctxt,
-    CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
+    CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
     ])
 *}
 
@@ -882,7 +879,7 @@
     DT ctxt "E" (atac),
     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
     DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
-    DT ctxt "H" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
+    DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
     ])
 *}