--- a/src/HOL/UNITY/UNITY_Main.thy	Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Wed Oct 20 20:25:33 2021 +0200
@@ -16,7 +16,7 @@
     "for proving safety properties"
 
 method_setup ensures_tac = \<open>
-  Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
+  Args.goal_spec -- Scan.lift Parse.embedded_inner_syntax >>
   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 \<close> "for proving progress properties"