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>