1.1 --- a/src/HOL/Integ/Bin.ML	Fri Nov 21 11:15:40 2003 +0100
     1.2 +++ b/src/HOL/Integ/Bin.ML	Mon Nov 24 15:33:07 2003 +0100
     1.3 @@ -250,8 +250,8 @@
     1.4  by (Simp_tac 1); 
     1.5  qed "iszero_number_of_Pls"; 
     1.6  
     1.7 -Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)"; 
     1.8 -by (Simp_tac 1);
     1.9 +Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)";
    1.10 +by (simp_tac (simpset() addsimps [eq_commute]) 1);
    1.11  qed "nonzero_number_of_Min"; 
    1.12  
    1.13  fun int_case_tac x = res_inst_tac [("z",x)] int_cases;