src/HOLCF/domain/theorems.ML

--- a/src/HOLCF/domain/theorems.ML	Mon Jun 13 21:28:57 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML	Tue Jun 14 03:35:15 2005 +0200
@@ -317,20 +317,18 @@
 val inverts =
   let
     val abs_less = ax_abs_iso RS (allI RS injection_less) RS iffD1;
-    val simps = [up_less, spair_less];
     val tacs = [
       dtac abs_less 1,
       REPEAT (dresolve_tac [sinl_less RS iffD1, sinr_less RS iffD1] 1),
-      asm_full_simp_tac (HOLCF_ss addsimps simps) 1];
+      asm_full_simp_tac (HOLCF_ss addsimps [spair_less]) 1];
   in map (fn (con,args) => pgterm (op <<) con args tacs) cons' end;
 val injects =
   let
     val abs_eq = ax_abs_iso RS (allI RS injection_eq) RS iffD1;
-    val simps = [up_eq, spair_eq];
     val tacs = [
       dtac abs_eq 1,
       REPEAT (dresolve_tac [sinl_inject, sinr_inject] 1),
-      asm_full_simp_tac (HOLCF_ss addsimps simps) 1];
+      asm_full_simp_tac (HOLCF_ss addsimps [spair_eq]) 1];
   in map (fn (con,args) => pgterm (op ===) con args tacs) cons' end;
 end;