# HG changeset patch
# User wenzelm
# Date 1329246575 -3600
# Node ID 4db76d47b51a19fac0dd38cf0b7d902af025e41c
# Parent  39e412f9ffdf975c6614b4ea717b1a172a72b86c
simplified use of tacticals;

diff -r 39e412f9ffdf -r 4db76d47b51a src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Feb 14 20:08:59 2012 +0100
+++ b/src/HOL/Quotient.thy	Tue Feb 14 20:09:35 2012 +0100
@@ -738,41 +738,41 @@
 
 method_setup lifting =
   {* Attrib.thms >> (fn thms => fn ctxt => 
-       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
+       SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms)) *}
   {* lift theorems to quotient types *}
 
 method_setup lifting_setup =
   {* Attrib.thm >> (fn thm => fn ctxt => 
-       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
+       SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm)) *}
   {* set up the three goals for the quotient lifting procedure *}
 
 method_setup descending =
-  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt [])) *}
   {* decend theorems to the raw level *}
 
 method_setup descending_setup =
-  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt [])) *}
   {* set up the three goals for the decending theorems *}
 
 method_setup partiality_descending =
-  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_tac ctxt []))) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt [])) *}
   {* decend theorems to the raw level *}
 
 method_setup partiality_descending_setup =
   {* Scan.succeed (fn ctxt => 
-       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))) *}
+       SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt [])) *}
   {* set up the three goals for the decending theorems *}
 
 method_setup regularize =
-  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt)) *}
   {* prove the regularization goals from the quotient lifting procedure *}
 
 method_setup injection =
-  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt)) *}
   {* prove the rep/abs injection goals from the quotient lifting procedure *}
 
 method_setup cleaning =
-  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
+  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt)) *}
   {* prove the cleaning goals from the quotient lifting procedure *}
 
 attribute_setup quot_lifted =
diff -r 39e412f9ffdf -r 4db76d47b51a src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Feb 14 20:08:59 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Feb 14 20:09:35 2012 +0100
@@ -364,7 +364,7 @@
   | (_ $
       (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
       (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
-        => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+        => rtac @{thm babs_rsp} THEN' quotient_tac ctxt
 
   | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
      (rtac @{thm refl} ORELSE'