# HG changeset patch
# User wenzelm
# Date 1170023356 -3600
# Node ID 0544af1a5117b0f9ab766a9ec3cff55cd3d5c58c
# Parent  6fe46a7259ec49e8a53fd3e3fa3d5dfe3f1ec2a4
added simproc_setup;

diff -r 6fe46a7259ec -r 0544af1a5117 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Jan 28 23:29:15 2007 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Jan 28 23:29:16 2007 +0100
@@ -20,6 +20,7 @@
   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 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 ->
@@ -238,6 +239,16 @@
   #> Context.proof_map;
 
 
+(* simprocs *)
+
+fun simproc_setup (name, pats, proc) =
+  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
+  |> Context.proof_map;
+
+
 (* goals *)
 
 fun goal opt_chain goal stmt int =
diff -r 6fe46a7259ec -r 0544af1a5117 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Jan 28 23:29:15 2007 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Jan 28 23:29:16 2007 +0100
@@ -311,6 +311,12 @@
     (P.opt_target -- P.text
     >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
 
+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))));
+
 
 (* translation functions *)
 
@@ -929,9 +935,10 @@
   constdefsP, definitionP, abbreviationP, notationP, axiomatizationP,
   theoremsP, lemmasP, declareP, globalP, localP, hideP, useP, mlP,
   ml_commandP, ml_setupP, setupP, method_setupP, declarationP,
-  parse_ast_translationP, parse_translationP, print_translationP,
-  typed_print_translationP, print_ast_translationP,
-  token_translationP, oracleP, contextP, localeP,
+  simproc_setupP, parse_ast_translationP, parse_translationP,
+  print_translationP, typed_print_translationP,
+  print_ast_translationP, token_translationP, oracleP, contextP,
+  localeP,
   (*proof commands*)
   theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
   assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,