src/HOL/Complex/CStar.ML

--- a/src/HOL/Complex/CStar.ML	Wed Jan 28 17:01:01 2004 +0100
+++ b/src/HOL/Complex/CStar.ML	Thu Jan 29 16:51:17 2004 +0100
@@ -95,7 +95,7 @@
 
 Goal "*sc* (A - B) = *sc* A - *sc* B";
 by (auto_tac (claset(),simpset() addsimps 
-         [set_diff_iff2,STARC_Int,STARC_Compl]));
+         [Diff_eq,STARC_Int,STARC_Compl]));
 qed "STARC_diff";
 
 Goalw [starsetC_n_def]