# HG changeset patch
# User wenzelm
# Date 908969341 -7200
# Node ID 21706a735c8d0ff026d48ab3a2bbc4b0008d1970
# Parent  56f2030c46c6734ca8057a5a016156e56ade79e7
record_split_name;

diff -r 56f2030c46c6 -r 21706a735c8d src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Client.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -19,7 +19,7 @@
 
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Addsimps [Cli_prg_def RS def_prg_Init];
 program_defs_ref := [Cli_prg_def];
diff -r 56f2030c46c6 -r 21706a735c8d src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -9,7 +9,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Delsimps [split_paired_All];
 
diff -r 56f2030c46c6 -r 21706a735c8d src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -9,7 +9,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
 program_defs_ref := [F_def, G_def];
diff -r 56f2030c46c6 -r 21706a735c8d src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -12,7 +12,7 @@
 
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Delsimps [split_paired_All];
 
diff -r 56f2030c46c6 -r 21706a735c8d src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Wed Oct 21 13:01:17 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Wed Oct 21 13:29:01 1998 +0200
@@ -7,7 +7,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "record_split_tac";
+claset_ref() := claset() delSWrapper record_split_name;
 
 Addsimps [Mprg_def RS def_prg_Init];
 program_defs_ref := [Mprg_def];