src/HOL/Library/Reflection.thy
changeset 30510 4120fc59dd85
parent 29650 cc3958d31b1d
child 30549 d2d7874648bd
     1.1 --- a/src/HOL/Library/Reflection.thy	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/HOL/Library/Reflection.thy	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  method_setup reify = {* fn src =>
     1.5    Method.syntax (Attrib.thms --
     1.6      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
     1.7 -  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
     1.8 +  (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
     1.9  *} "partial automatic reification"
    1.10  
    1.11  method_setup reflection = {* 
    1.12 @@ -38,7 +38,7 @@
    1.13          val (ceqs,cths) = Reify_Data.get ctxt 
    1.14          val corr_thms = ths@cths
    1.15          val raw_eqs = eqs@ceqs
    1.16 -      in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
    1.17 +      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
    1.18       end) end
    1.19  *} "reflection method"
    1.20