src/HOLCF/IOA/meta_theory/Abstraction.thy
changeset 30607 c3d1590debd8
parent 27208 5fe899199f85
child 31738 7b9b9ba532ca
     1.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOLCF/IOA/meta_theory/Abstraction.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Olaf Müller
     1.7  *)
     1.8  
     1.9 @@ -605,12 +604,15 @@
    1.10    strength_Diamond strength_Leadsto weak_WF weak_SF
    1.11  
    1.12  ML {*
    1.13 -fun abstraction_tac i =
    1.14 -    SELECT_GOAL (CLASIMPSET (fn (cs, ss) =>
    1.15 -      auto_tac (cs addSIs @{thms weak_strength_lemmas},
    1.16 -        ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))) i
    1.17 +fun abstraction_tac ctxt =
    1.18 +  let val (cs, ss) = local_clasimpset_of ctxt in
    1.19 +    SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
    1.20 +        ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
    1.21 +  end
    1.22  *}
    1.23  
    1.24 +method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
    1.25 +
    1.26  use "ioa_package.ML"
    1.27  
    1.28  end