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 _ =