more robust syntax;
authorwenzelm
Wed, 26 May 2021 18:07:49 +0200
changeset 73787 493b1ae188da
parent 73786 18d80cd51823
child 73788 35217bf33215
child 73790 370ce138d1bd
more robust syntax;
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 _ =