--- a/src/HOL/UNITY/UNITY_Main.thy Thu May 12 18:17:32 2011 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Thu May 12 18:18:06 2011 +0200
@@ -11,13 +11,12 @@
begin
method_setup safety = {*
- Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (constrains_tac (clasimpset_of ctxt))) *}
+ Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
"for proving safety properties"
method_setup ensures_tac = {*
Args.goal_spec -- Scan.lift Args.name_source >>
- (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (clasimpset_of ctxt) s))
+ (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
*} "for proving progress properties"
end