# HG changeset patch
# User paulson
# Date 934822040 -7200
# Node ID 13e43b7456a1de6fa14ccbfcfa2f05fe59cea0b6
# Parent  da6f387ca482014195ea5929beb714cb348a739f
deleted obsolete assignment

diff -r da6f387ca482 -r 13e43b7456a1 src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Mon Aug 16 18:43:13 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Mon Aug 16 18:47:20 1999 +0200
@@ -8,9 +8,6 @@
 From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
 *)
 
-(*split_all_tac causes a big blow-up*)
-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 da6f387ca482 -r 13e43b7456a1 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Mon Aug 16 18:43:13 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML	Mon Aug 16 18:47:20 1999 +0200
@@ -6,9 +6,6 @@
 The Lift-Control Example
 *)
 
-(*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper record_split_name;
-
 Goal "[| x ~: A;  y : A |] ==> x ~= y";
 by (Blast_tac 1);
 qed "not_mem_distinct";
diff -r da6f387ca482 -r 13e43b7456a1 src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Mon Aug 16 18:43:13 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Mon Aug 16 18:47:20 1999 +0200
@@ -6,9 +6,6 @@
 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
 *)
 
-(*record_split_name causes a BIG blow-up (doubles the run-time)*)
-claset_ref() := claset() delSWrapper record_split_name;
-
 Addsimps [Mutex_def RS def_prg_Init];
 program_defs_ref := [Mutex_def];