src/FOL/FOL.thy
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!)"