src/Pure/Pure.thy
changeset 73787 493b1ae188da
parent 73312 736b8853189a
child 74171 a9e79c3645c4
--- a/src/Pure/Pure.thy	Tue May 25 23:58:49 2021 +0200
+++ b/src/Pure/Pure.thy	Wed May 26 18:07:49 2021 +0200
@@ -296,7 +296,7 @@
 
 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 _ =