src/HOL/Tools/record_package.ML

  *   X does not affect the selected subrecord.
  * - If X is a more-selector we have to make sure that S is not in the updated
  *   subrecord.
  *)
 val record_simproc =
-  Simplifier.simproc HOL.thy "record_simp" ["s (u k r)"]   (* FIXME pattern!? *)
+  Simplifier.simproc HOL.thy "record_simp" ["x"]
     (fn sg => fn ss => fn t =>
       (case t of (sel as Const (s, Type (_,[domS,rangeS])))$
                    ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
         if is_selector sg s then
           (case get_updates sg u of SOME u_name =>

  *    r(|more := m; A := A r|)
  * If A is contained in the fields of m we cannot remove the update A := A r!
  * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|)
 *)
 val record_upd_simproc =
-  Simplifier.simproc HOL.thy "record_upd_simp" ["u k r"]    (* FIXME pattern *)
+  Simplifier.simproc HOL.thy "record_upd_simp" ["x"]
     (fn sg => fn ss => fn t =>
       (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
          let datatype ('a,'b) calc = Init of 'b | Inter of 'a
              val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
 

  * P t = 0: do not split
  * P t = ~1: completely split
  * P t > 0: split up to given bound of record extensions
  *)
 fun record_split_simproc P =
-  Simplifier.simproc HOL.thy "record_split_simp" ["a t"]
+  Simplifier.simproc HOL.thy "record_split_simp" ["x"]
     (fn sg => fn _ => fn t =>
       (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
          if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
          then (case rec_id (~1) T of
                  "" => NONE