delSWrapper "record_split_tac";

--- a/src/HOL/UNITY/Client.ML	Tue Oct 20 16:41:50 1998 +0200
+++ b/src/HOL/UNITY/Client.ML	Tue Oct 20 17:27:00 1998 +0200
@@ -19,7 +19,7 @@
 
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "split_all_tac";
+claset_ref() := claset() delSWrapper "record_split_tac";
 
 Addsimps [Cli_prg_def RS def_prg_Init];
 program_defs_ref := [Cli_prg_def];

--- a/src/HOL/UNITY/Comp.ML	Tue Oct 20 16:41:50 1998 +0200
+++ b/src/HOL/UNITY/Comp.ML	Tue Oct 20 17:27:00 1998 +0200
@@ -9,7 +9,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "split_all_tac";
+claset_ref() := claset() delSWrapper "record_split_tac";
 
 Delsimps [split_paired_All];
 

--- a/src/HOL/UNITY/Handshake.ML	Tue Oct 20 16:41:50 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Tue Oct 20 17:27:00 1998 +0200
@@ -9,7 +9,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "split_all_tac";
+claset_ref() := claset() delSWrapper "record_split_tac";
 
 Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
 program_defs_ref := [F_def, G_def];

--- a/src/HOL/UNITY/Lift.ML	Tue Oct 20 16:41:50 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Tue Oct 20 17:27:00 1998 +0200
@@ -12,7 +12,7 @@
 
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "split_all_tac";
+claset_ref() := claset() delSWrapper "record_split_tac";
 
 Delsimps [split_paired_All];
 

--- a/src/HOL/UNITY/Mutex.ML	Tue Oct 20 16:41:50 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Tue Oct 20 17:27:00 1998 +0200
@@ -7,7 +7,7 @@
 *)
 
 (*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper "split_all_tac";
+claset_ref() := claset() delSWrapper "record_split_tac";
 
 Addsimps [Mprg_def RS def_prg_Init];
 program_defs_ref := [Mprg_def];