changeset 74563 | 042041c0ebeb |
parent 74300 | 33f13d2d211c |
child 80701 | 39cd50407f79 |
--- a/src/FOL/FOL.thy Wed Oct 20 20:04:28 2021 +0200 +++ b/src/FOL/FOL.thy Wed Oct 20 20:25:33 2021 +0200 @@ -72,7 +72,7 @@ \<close> method_setup case_tac = \<open> - Args.goal_spec -- Scan.lift (Args.embedded_inner_syntax -- Parse.for_fixes) >> + Args.goal_spec -- Scan.lift (Parse.embedded_inner_syntax -- Parse.for_fixes) >> (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes)) \<close> "case_tac emulation (dynamic instantiation!)"