# HG changeset patch
# User wenzelm
# Date 1135207729 -3600
# Node ID a081b771392c1beae4f71ccee053446ebe9726a1
# Parent  56414918dbbd76447517ef5a2149859286fbcac8
induct_rulify;

diff -r 56414918dbbd -r a081b771392c src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Dec 22 00:28:47 2005 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Dec 22 00:28:49 2005 +0100
@@ -1105,7 +1105,7 @@
 
 local
 val inductive_atomize = thms "induct_atomize";
-val inductive_rulify1 = thms "induct_rulify1";
+val inductive_rulify = thms "induct_rulify";
 in
 (* record_split_simp_tac *)
 (* splits (and simplifies) all records in the goal for which P holds.
@@ -1135,7 +1135,7 @@
             val thm  = cterm_instantiate [(crec,cfree)] induct_thm;
         in EVERY [simp_tac (HOL_basic_ss addsimps inductive_atomize) i,
                   rtac thm i,
-                  simp_tac (HOL_basic_ss addsimps inductive_rulify1) i]
+                  simp_tac (HOL_basic_ss addsimps inductive_rulify) i]
         end;
 
     fun split_free_tac P i (free as Free (n,T)) =