diff -r 8403bd51f8b1 -r 042041c0ebeb src/FOL/FOL.thy --- 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 @@ \ method_setup case_tac = \ - 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)) \ "case_tac emulation (dynamic instantiation!)"