proper binding/report of defined simprocs;
tuned signature;

--- a/src/Pure/Isar/args.ML	Sat Apr 23 13:00:19 2011 +0200
+++ b/src/Pure/Isar/args.ML	Sat Apr 23 13:53:09 2011 +0200
@@ -46,7 +46,8 @@
   val named_typ: (string -> typ) -> typ parser
   val named_term: (string -> term) -> term parser
   val named_fact: (string -> thm list) -> thm list parser
-  val named_attribute: (string -> morphism -> attribute) -> (morphism -> attribute) parser
+  val named_attribute:
+    (string * Position.T -> morphism -> attribute) -> (morphism -> attribute) parser
   val typ_abbrev: typ context_parser
   val typ: typ context_parser
   val term: term context_parser
@@ -176,10 +177,13 @@
 fun named_text intern = internal_text || named >> evaluate Token.Text (intern o Token.content_of);
 fun named_typ readT = internal_typ || named >> evaluate Token.Typ (readT o Token.source_of);
 fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.source_of);
+
 fun named_fact get = internal_fact || named >> evaluate Token.Fact (get o Token.content_of) ||
   alt_string >> evaluate Token.Fact (get o Token.source_of);
+
 fun named_attribute att =
-  internal_attribute || named >> evaluate Token.Attribute (att o Token.content_of);
+  internal_attribute ||
+  named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.position_of tok));
 
 
 (* terms and types *)

--- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 23 13:00:19 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 23 13:53:09 2011 +0200
@@ -20,8 +20,8 @@
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
   val declaration: {syntax: bool, pervasive: bool} ->
     Symbol_Pos.text * Position.T -> local_theory -> local_theory
-  val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
-    local_theory -> local_theory
+  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T ->
+    string list -> local_theory -> local_theory
   val hide_class: bool -> xstring list -> theory -> theory
   val hide_type: bool -> xstring list -> theory -> theory
   val hide_const: bool -> xstring list -> theory -> theory
@@ -214,7 +214,7 @@
   ML_Lex.read pos txt
   |> ML_Context.expression pos
     "val proc: Morphism.morphism -> Simplifier.simpset -> cterm -> thm option"
-    ("Context.map_proof (Simplifier.def_simproc {name = " ^ ML_Syntax.print_string name ^ ", \
+    ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
       \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
       \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
   |> Context.proof_map;

--- a/src/Pure/Isar/isar_syn.ML	Sat Apr 23 13:00:19 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 23 13:53:09 2011 +0200
@@ -349,7 +349,7 @@
 
 val _ =
   Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
-    (Parse.name --
+    (Parse.position Parse.name --
       (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
       Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
     >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));

--- a/src/Pure/simplifier.ML	Sat Apr 23 13:00:19 2011 +0200
+++ b/src/Pure/simplifier.ML	Sat Apr 23 13:53:09 2011 +0200
@@ -58,11 +58,11 @@
   val cong_add: attribute
   val cong_del: attribute
   val map_simpset: (simpset -> simpset) -> theory -> theory
-  val get_simproc: Context.generic -> xstring -> simproc
-  val def_simproc: {name: string, lhss: string list,
+  val get_simproc: Proof.context -> xstring * Position.T -> simproc
+  val def_simproc: {name: binding, lhss: term list,
     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
     local_theory -> local_theory
-  val def_simproc_i: {name: string, lhss: term list,
+  val def_simproc_cmd: {name: binding, lhss: string list,
     proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} ->
     local_theory -> local_theory
   val cong_modifiers: Method.modifier parser list
@@ -162,27 +162,28 @@
 
 (* get simprocs *)
 
-fun get_simproc context xname =
+fun get_simproc ctxt (xname, pos) =
   let
-    val (space, tab) = Simprocs.get context;
+    val (space, tab) = Simprocs.get (Context.Proof ctxt);
     val name = Name_Space.intern space xname;
   in
     (case Symtab.lookup tab name of
-      SOME proc => proc
+      SOME proc => (Context_Position.report ctxt pos (Name_Space.markup space name); proc)
     | NONE => error ("Undefined simplification procedure: " ^ quote name))
   end;
 
-val _ = ML_Antiquote.value "simproc" (Scan.lift Args.name >> (fn name =>
-  "Simplifier.get_simproc (ML_Context.the_generic_context ()) " ^ ML_Syntax.print_string name));
+val _ =
+  ML_Antiquote.value "simproc" (Scan.lift (Parse.position Args.name) >> (fn x =>
+    "Simplifier.get_simproc (ML_Context.the_local_context ()) " ^
+      ML_Syntax.print_pair ML_Syntax.print_string  ML_Syntax.print_position x));
 
 
 (* define simprocs *)
 
 local
 
-fun gen_simproc prep {name, lhss, proc, identifier} lthy =
+fun gen_simproc prep {name = b, lhss, proc, identifier} lthy =
   let
-    val b = Binding.name name;
     val naming = Local_Theory.naming_of lthy;
     val simproc = make_simproc
       {name = Name_Space.full_name naming b,
@@ -211,8 +212,8 @@
 
 in
 
-val def_simproc = gen_simproc Syntax.read_terms;
-val def_simproc_i = gen_simproc Syntax.check_terms;
+val def_simproc = gen_simproc Syntax.check_terms;
+val def_simproc_cmd = gen_simproc Syntax.read_terms;
 
 end;
 
@@ -310,7 +311,7 @@
 val simproc_att =
   Scan.peek (fn context =>
     add_del :|-- (fn decl =>
-      Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
+      Scan.repeat1 (Args.named_attribute (decl o get_simproc (Context.proof_of context)))
       >> (Library.apply o map Morphism.form)));
 
 end;