author | wenzelm |
Wed, 26 May 2021 18:07:49 +0200 | |
changeset 74043 | 493b1ae188da |
parent 74042 | 18d80cd51823 |
child 74044 | 370ce138d1bd |
child 74046 | 35217bf33215 |
src/Pure/Pure.thy | file | annotate | diff | comparison | revisions |
--- 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 _ =