src/Pure/Pure.thy

   Outer_Syntax.local_theory \<^command_keyword>\<open>local_setup\<close> "ML setup for local theory"
     (Parse.ML_source >> Isar_Cmd.local_setup);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>oracle\<close> "declare oracle"
-    (Parse.range Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.ML_source) >>
+    (Parse.range Parse.name -- Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source) >>
       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>attribute_setup\<close> "define attribute in ML"
     (Parse.name_position --