# HG changeset patch
# User wenzelm
# Date 1127507482 -7200
# Node ID f526e2b9fe9ed0c3bef79af984e40403d81e8187
# Parent  3c5b158be33c6a4106e44d369b696691e3399494
simprocs: pattern now "x" (the proc is supposed to discriminate faster than Pattern.match);

diff -r 3c5b158be33c -r f526e2b9fe9e src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Sep 23 22:21:55 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Sep 23 22:31:22 2005 +0200
@@ -849,7 +849,7 @@
  *   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)=>
@@ -910,7 +910,7 @@
  * (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
@@ -1041,7 +1041,7 @@
  * 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"