# HG changeset patch
# User wenzelm
# Date 908897220 -7200
# Node ID e57980ec351b3a1955802b2babe2eca2a530e24a
# Parent  491944c2fb123ee38f164742caacd32973460a0f
delSWrapper "record_split_tac";

diff -r 491944c2fb12 -r e57980ec351b src/HOL/UNITY/Client.ML
--- 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];
diff -r 491944c2fb12 -r e57980ec351b src/HOL/UNITY/Comp.ML
--- 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];
 
diff -r 491944c2fb12 -r e57980ec351b src/HOL/UNITY/Handshake.ML
--- 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];
diff -r 491944c2fb12 -r e57980ec351b src/HOL/UNITY/Lift.ML
--- 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];
 
diff -r 491944c2fb12 -r e57980ec351b src/HOL/UNITY/Mutex.ML
--- 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];