src/HOL/Quotient.thy
changeset 38859 053c69cb4a0e
parent 38702 72fd257f4343
child 38861 27c7b620758c
     1.1 --- a/src/HOL/Quotient.thy	Sat Aug 28 11:42:33 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Sat Aug 28 20:24:40 2010 +0800
     1.3 @@ -773,20 +773,20 @@
     1.4  
     1.5  method_setup lifting =
     1.6    {* Attrib.thms >> (fn thms => fn ctxt => 
     1.7 -       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
     1.8 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
     1.9    {* lifts theorems to quotient types *}
    1.10  
    1.11  method_setup lifting_setup =
    1.12    {* Attrib.thm >> (fn thm => fn ctxt => 
    1.13 -       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
    1.14 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
    1.15    {* sets up the three goals for the quotient lifting procedure *}
    1.16  
    1.17  method_setup descending =
    1.18 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
    1.19 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
    1.20    {* decends theorems to the raw level *}
    1.21  
    1.22  method_setup descending_setup =
    1.23 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *}
    1.24 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
    1.25    {* sets up the three goals for the decending theorems *}
    1.26  
    1.27  method_setup regularize =