--- a/src/Pure/Isar/isar_syn.ML Thu Jul 14 19:28:32 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Jul 14 19:28:33 2005 +0200
@@ -292,8 +292,9 @@
(* oracles *)
val oracleP =
- OuterSyntax.command "oracle" "install oracle" K.thy_decl
- ((P.name --| P.$$$ "=") -- P.text >> (Toplevel.theory o IsarThy.add_oracle));
+ OuterSyntax.command "oracle" "declare oracle" K.thy_decl
+ (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
+ -- P.text >> (Toplevel.theory o IsarThy.add_oracle o P.triple1));
(* locales *)