tuned oracle interface;
simproc_setup: added identifier;

--- a/src/Pure/Isar/isar_cmd.ML	Sun Feb 04 22:02:18 2007 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Feb 04 22:02:19 2007 +0100
@@ -14,13 +14,13 @@
   val typed_print_translation: bool * string -> theory -> theory
   val print_ast_translation: bool * string -> theory -> theory
   val token_translation: string -> theory -> theory
-  val oracle: bstring * string * string -> theory -> theory
+  val oracle: bstring -> string -> string -> theory -> theory
   val add_axioms: ((bstring * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((bstring * string) * Attrib.src list) list -> theory -> theory
   val apply_theorems: (thmref * Attrib.src list) list -> theory -> thm list * theory
   val apply_theorems_i: (thm list * attribute list) list -> theory -> thm list * theory
   val declaration: string -> local_theory -> local_theory
-  val simproc_setup: string * string list * string -> local_theory -> local_theory
+  val simproc_setup: string -> string list -> string -> string list -> local_theory -> local_theory
   val have: ((string * Attrib.src list) * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
   val hence: ((string * Attrib.src list) * (string * string list) list) list ->
@@ -192,10 +192,10 @@
 
 (* oracles *)
 
-fun oracle (name, T, oracle) =
+fun oracle name typ oracle =
   let val txt =
     "local\n\
-    \  type T = " ^ T ^ ";\n\
+    \  type T = " ^ typ ^ ";\n\
     \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
     \  val name = " ^ quote name ^ ";\n\
     \  exception Arg of T;\n\
@@ -241,11 +241,12 @@
 
 (* simprocs *)
 
-fun simproc_setup (name, pats, proc) =
+fun simproc_setup name lhss proc identifier =
   ML_Context.use_let
-    "val simproc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
-  ("Context.map_proof (Simplifier.def_simproc " ^ ML_Syntax.print_string name ^ " " ^
-    ML_Syntax.print_list ML_Syntax.print_string pats ^ " simproc)") proc
+    "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
+  ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
+    \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
+    \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") proc
   |> Context.proof_map;
 
 

--- a/src/Pure/Isar/isar_syn.ML	Sun Feb 04 22:02:18 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Feb 04 22:02:19 2007 +0100
@@ -314,8 +314,9 @@
 val simproc_setupP =
   OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl)
     (P.opt_target --
-      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text
-    >> (fn (((loc, x), y), z) => Toplevel.local_theory loc (IsarCmd.simproc_setup (x, y, z))));
+      P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.text --
+      Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) []
+    >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d)));
 
 
 (* translation functions *)
@@ -358,7 +359,7 @@
 val oracleP =
   OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
     (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
-      -- P.text >> (Toplevel.theory o IsarCmd.oracle o P.triple1));
+      -- P.text >> (fn ((x, y), z) => Toplevel.theory (IsarCmd.oracle x y z)));
 
 
 (* local theories *)
@@ -913,14 +914,14 @@
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
 val _ = OuterSyntax.add_keywords
- ["!", "!!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
-  "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes", "attach",
-  "begin", "binder", "concl", "constrains", "defines", "fixes", "for",
-  "imports", "if", "in", "includes", "infix", "infixl", "infixr",
-  "is", "notes", "obtains", "open", "output", "overloaded", "shows",
-  "structure", "unchecked", "uses", "where", "|", "\\<equiv>",
-  "\\<leftharpoondown>", "\\<rightharpoonup>",
-  "\\<rightleftharpoons>", "\\<subseteq>"];
+ ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
+  "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
+  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
+  "advanced", "and", "assumes", "attach", "begin", "binder", "concl",
+  "constrains", "defines", "fixes", "for", "identifier", "if",
+  "imports", "in", "includes", "infix", "infixl", "infixr", "is",
+  "notes", "obtains", "open", "output", "overloaded", "shows",
+  "structure", "unchecked", "uses", "where", "|"];
 
 val _ = OuterSyntax.add_parsers [
   (*theory structure*)