# HG changeset patch
# User wenzelm
# Date 1622045269 -7200
# Node ID 493b1ae188dadd3c43a5b6d66c1c99f6cccf10f9
# Parent  18d80cd51823f86ef69870dfe977c3e1f1bcc556
more robust syntax;

diff -r 18d80cd51823 -r 493b1ae188da src/Pure/Pure.thy
--- 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 _ =