1.1 --- a/src/HOL/GroupTheory/Exponent.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/GroupTheory/Exponent.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -205,13 +205,13 @@
     1.4  by (induct_tac "n" 1);
     1.5  by (Asm_simp_tac 1); 
     1.6  by (Asm_full_simp_tac 1); 
     1.7 -by (subgoal_tac "# 2 * n + # 2 <= p * p^n" 1);
     1.8 +by (subgoal_tac "2 * n + 2 <= p * p^n" 1);
     1.9  by (Asm_full_simp_tac 1); 
    1.10 -by (subgoal_tac "# 2 * p^n <= p * p^n" 1);
    1.11 +by (subgoal_tac "2 * p^n <= p * p^n" 1);
    1.12  (*?arith_tac should handle all of this!*)
    1.13  by (rtac order_trans 1); 
    1.14  by (assume_tac 2); 
    1.15 -by (dres_inst_tac [("k","# 2")] mult_le_mono2 1); 
    1.16 +by (dres_inst_tac [("k","2")] mult_le_mono2 1); 
    1.17  by (Asm_full_simp_tac 1); 
    1.18  by (rtac mult_le_mono1 1); 
    1.19  by (Asm_full_simp_tac 1);