src/HOL/Library/Reflection.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 31412 f2e6b6526092
     1.1 --- a/src/HOL/Library/Reflection.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Library/Reflection.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -16,10 +16,10 @@
     1.4  
     1.5  use "reflection.ML"
     1.6  
     1.7 -method_setup reify = {* fn src =>
     1.8 -  Method.syntax (Attrib.thms --
     1.9 -    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
    1.10 -  (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    1.11 +method_setup reify = {*
    1.12 +  Attrib.thms --
    1.13 +    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
    1.14 +  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    1.15  *} "partial automatic reification"
    1.16  
    1.17  method_setup reflection = {* 
    1.18 @@ -30,16 +30,17 @@
    1.19    val any_keyword = keyword onlyN || keyword rulesN;
    1.20    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    1.21    val terms = thms >> map (term_of o Drule.dest_term);
    1.22 -  fun optional scan = Scan.optional scan [];
    1.23 -in fn src =>
    1.24 -  Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
    1.25 -    (fn (((eqs,ths),to), ctxt) => 
    1.26 -      let 
    1.27 -        val (ceqs,cths) = Reify_Data.get ctxt 
    1.28 -        val corr_thms = ths@cths
    1.29 -        val raw_eqs = eqs@ceqs
    1.30 -      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
    1.31 -     end) end
    1.32 -*} "reflection method"
    1.33 +in
    1.34 +  thms --
    1.35 +  Scan.optional (keyword rulesN |-- thms) [] --
    1.36 +  Scan.option (keyword onlyN |-- Args.term) >>
    1.37 +  (fn ((eqs,ths),to) => fn ctxt =>
    1.38 +    let 
    1.39 +      val (ceqs,cths) = Reify_Data.get ctxt 
    1.40 +      val corr_thms = ths@cths
    1.41 +      val raw_eqs = eqs@ceqs
    1.42 +    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
    1.43 +end
    1.44 +*} "reflection"
    1.45  
    1.46  end