| changeset 63120 | 629a4c5e953e |
| parent 58889 | 5b7a9633cfa8 |
| child 63146 | f1ecba0272f9 |
--- a/src/HOL/UNITY/UNITY_Main.thy Mon May 23 20:45:10 2016 +0200 +++ b/src/HOL/UNITY/UNITY_Main.thy Mon May 23 21:30:30 2016 +0200 @@ -16,7 +16,7 @@ "for proving safety properties" method_setup ensures_tac = {* - Args.goal_spec -- Scan.lift Args.name_inner_syntax >> + Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >> (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) *} "for proving progress properties"