--- a/src/HOLCF/HOLCF.ML Mon Dec 09 19:11:11 1996 +0100
+++ b/src/HOLCF/HOLCF.ML Mon Dec 09 19:13:13 1996 +0100
@@ -6,7 +6,4 @@
open HOLCF;
-Addsimps (one_when @ dist_less_one @ dist_eq_one @ dist_less_tr @ dist_eq_tr
- @ tr_when @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms);
-
val HOLCF_ss = !simpset;
--- a/src/HOLCF/One.ML Mon Dec 09 19:11:11 1996 +0100
+++ b/src/HOLCF/One.ML Mon Dec 09 19:13:13 1996 +0100
@@ -96,3 +96,4 @@
val one_when = map prover ["one_when`x`UU = UU","one_when`x`one = x"];
+Addsimps (one_when @ dist_less_one @ dist_eq_one);
\ No newline at end of file
--- a/src/HOLCF/Tr2.ML Mon Dec 09 19:11:11 1996 +0100
+++ b/src/HOLCF/Tr2.ML Mon Dec 09 19:13:13 1996 +0100
@@ -92,7 +92,8 @@
"If FF then e1 else e2 fi = e2",
"If TT then e1 else e2 fi = e1"];
-
+Addsimps (dist_less_tr @ dist_eq_tr @ tr_when @ andalso_thms @
+ orelse_thms @ neg_thms @ ifte_thms);