tuned whitespace
authorhaftmann
Fri Mar 02 18:26:54 2012 +0100 (2012-03-02)
changeset 4676507f9eda810b3
parent 46764 a65e18ceb1e3
child 46766 4269ae06afc5
tuned whitespace
src/HOL/Library/Reflection.thy
     1.1 --- a/src/HOL/Library/Reflection.thy	Fri Mar 02 15:18:05 2012 +0100
     1.2 +++ b/src/HOL/Library/Reflection.thy	Fri Mar 02 18:26:54 2012 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  method_setup reify = {*
     1.5    Attrib.thms --
     1.6      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
     1.7 -  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
     1.8 +  (fn (eqs, to) => fn 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 @@ -31,11 +31,11 @@
    1.13    thms --
    1.14    Scan.optional (keyword rulesN |-- thms) [] --
    1.15    Scan.option (keyword onlyN |-- Args.term) >>
    1.16 -  (fn ((eqs,ths),to) => fn ctxt =>
    1.17 +  (fn ((eqs, ths), to) => fn ctxt =>
    1.18      let
    1.19 -      val (ceqs,cths) = Reify_Data.get ctxt
    1.20 -      val corr_thms = ths@cths
    1.21 -      val raw_eqs = eqs@ceqs
    1.22 +      val (ceqs, cths) = Reify_Data.get ctxt
    1.23 +      val corr_thms = ths @ cths
    1.24 +      val raw_eqs = eqs @ ceqs
    1.25      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
    1.26  end
    1.27  *}