src/HOL/Subst/Unifier.ML

--- a/src/HOL/Subst/Unifier.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/Subst/Unifier.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -82,8 +82,7 @@
 
 goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])";
 by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
-				 empty_iff_all_not]
-                       addsplits [expand_if]) 1);
+				 empty_iff_all_not]) 1);
 by (Blast_tac 1);
 qed_spec_mp "Var_Idem";