src/HOL/HOLCF/IOA/CompoScheds.thy
changeset 74563 042041c0ebeb
parent 69597 ff784d5a5bfb
--- a/src/HOL/HOLCF/IOA/CompoScheds.thy	Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/HOLCF/IOA/CompoScheds.thy	Wed Oct 20 20:25:33 2021 +0200
@@ -289,7 +289,7 @@
 \<close>
 
 method_setup mkex_induct = \<open>
-  Scan.lift (Args.embedded -- Args.embedded -- Args.embedded)
+  Scan.lift (Parse.embedded -- Parse.embedded -- Parse.embedded)
     >> (fn ((sch, exA), exB) => fn ctxt =>
       SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
 \<close>