# HG changeset patch
# User wenzelm
# Date 1397132855 -7200
# Node ID 34ea4d7f236c52079e70a3ceaad7363dfe7864ff
# Parent  9276da80f7c3996a0f73ce08245769058fac3581
more standard names;

diff -r 9276da80f7c3 -r 34ea4d7f236c src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Thu Apr 10 12:48:01 2014 +0200
+++ b/src/HOL/Tools/record.ML	Thu Apr 10 14:27:35 2014 +0200
@@ -1066,7 +1066,7 @@
     subrecord.
 *)
 val simproc =
-  Simplifier.simproc_global @{theory HOL} "record_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record" ["x"]
     (fn ctxt => fn t =>
       let val thy = Proof_Context.theory_of ctxt in
         (case t of
@@ -1142,7 +1142,7 @@
   we omit considering further updates if doing so would introduce
   both a more update and an update to a field within it.*)
 val upd_simproc =
-  Simplifier.simproc_global @{theory HOL} "record_upd_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record_upd" ["x"]
     (fn ctxt => fn t =>
       let
         val thy = Proof_Context.theory_of ctxt;
@@ -1263,7 +1263,7 @@
  Complexity: #components * #updates     #updates
 *)
 val eq_simproc =
-  Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
+  Simplifier.simproc_global @{theory HOL} "record_eq" ["r = s"]
     (fn ctxt => fn t =>
       (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
         (case rec_id ~1 T of
@@ -1283,7 +1283,7 @@
     P t = ~1: completely split
     P t > 0: split up to given bound of record extensions.*)
 fun split_simproc P =
-  Simplifier.simproc_global @{theory HOL} "record_split_simp" ["x"]
+  Simplifier.simproc_global @{theory HOL} "record_split" ["x"]
     (fn ctxt => fn t =>
       (case t of
         Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
@@ -1311,7 +1311,7 @@
       | _ => NONE));
 
 val ex_sel_eq_simproc =
-  Simplifier.simproc_global @{theory HOL} "ex_sel_eq_simproc" ["Ex t"]
+  Simplifier.simproc_global @{theory HOL} "ex_sel_eq" ["Ex t"]
     (fn ctxt => fn t =>
       let
         val thy = Proof_Context.theory_of ctxt;