src/HOL/ex/Reflection.thy
changeset 21588 cd0dc678a205
parent 20374 01b711328990
child 21879 a3efbae45735
     1.1 --- a/src/HOL/ex/Reflection.thy	Wed Nov 29 15:44:46 2006 +0100
     1.2 +++ b/src/HOL/ex/Reflection.thy	Wed Nov 29 15:44:51 2006 +0100
     1.3 @@ -18,14 +18,14 @@
     1.4    fn src =>
     1.5      Method.syntax (Attrib.thms --
     1.6        Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
     1.7 -  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.genreify_tac ctxt eqs to))
     1.8 +  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
     1.9  *} "partial automatic reification"
    1.10  
    1.11  method_setup reflection = {*
    1.12    fn src =>
    1.13      Method.syntax (Attrib.thms --
    1.14        Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    1.15 -  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.reflection_tac ctxt ths to))
    1.16 +  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
    1.17  *} "reflection method"
    1.18  
    1.19  end