more robust read_simproc_spec: proper error positions;

--- a/src/Pure/simplifier.ML	Sat Oct 21 11:34:37 2023 +0200
+++ b/src/Pure/simplifier.ML	Sat Oct 21 12:02:23 2023 +0200
@@ -39,10 +39,12 @@
   val the_simproc: Proof.context -> string -> simproc
   val make_simproc: Proof.context -> string ->
     {lhss: term list, proc: morphism -> proc} -> simproc
-  type 'a simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: morphism -> proc}
-  val define_simproc: term simproc_spec -> local_theory -> simproc * local_theory
-  val simproc_setup: term simproc_spec -> simproc
-  val simproc_setup_cmd: string simproc_spec -> simproc
+  type ('a, 'b) simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: 'b}
+  val read_simproc_spec: Proof.context -> (string, 'a) simproc_spec -> (term, 'a) simproc_spec
+  val define_simproc: (term, morphism -> proc) simproc_spec -> local_theory ->
+    simproc * local_theory
+  val simproc_setup: (term, morphism -> proc) simproc_spec -> simproc
+  val simproc_setup_cmd: (string, morphism -> proc) simproc_spec -> simproc
   val simproc_setup_command: (local_theory -> local_theory) parser
   val pretty_simpset: bool -> Proof.context -> Pretty.T
   val default_mk_sym: Proof.context -> thm -> thm option
@@ -132,7 +134,14 @@
       {lhss = lhss', proc = Morphism.entity proc}
   end;
 
-type 'a simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: morphism -> proc};
+type ('a, 'b) simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: 'b};
+
+fun read_simproc_spec ctxt {passive, name, lhss, proc} : (term, 'a) simproc_spec =
+  let
+    val lhss' =
+      Syntax.read_terms ctxt lhss handle ERROR msg =>
+        error (msg ^ Position.here_list (map Syntax.read_input_pos lhss));
+  in {passive = passive, name = name, lhss = lhss', proc = proc} end;
 
 fun define_simproc {passive, name, lhss, proc} lthy =
   let
@@ -158,10 +167,9 @@
 val simproc_setup =
   Named_Target.setup_result Raw_Simplifier.transform_simproc o define_simproc;
 
-fun simproc_setup_cmd {passive, name, lhss, proc} =
-  Named_Target.setup_result Raw_Simplifier.transform_simproc (fn lthy =>
-    lthy |> define_simproc
-      {passive = passive, name = name, lhss = Syntax.read_terms lthy lhss, proc = proc});
+fun simproc_setup_cmd args =
+  Named_Target.setup_result Raw_Simplifier.transform_simproc
+    (fn lthy => lthy |> define_simproc (read_simproc_spec lthy args));
 
 val simproc_setup_parser =
   Scan.optional (Parse.$$$ "passive" >> K true) false --
@@ -177,8 +185,8 @@
         val ml = ML_Lex.tokenize_no_range;
 
         val {passive, name, lhss, proc} = input
-          |> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) simproc_setup_parser;
-        val lhss' = Syntax.read_terms ctxt lhss;
+          |> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) simproc_setup_parser
+          |> read_simproc_spec ctxt;
 
         val (decl, ctxt') = ML_Context.read_antiquotes proc ctxt;
         fun decl' ctxt'' =
@@ -187,7 +195,7 @@
             val ml_body' =
               ml "Simplifier.simproc_setup {passive = " @ ml (Bool.toString passive) @
               ml ", name = " @ ml (ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name)) @
-              ml ", lhss = " @ ml (ML_Syntax.print_list ML_Syntax.print_term lhss') @
+              ml ", lhss = " @ ml (ML_Syntax.print_list ML_Syntax.print_term lhss) @
               ml ", proc = (" @ ml_body @ ml ")}";
           in (ml_env, ml_body') end;
       in (decl', ctxt') end));