src/HOL/ex/Fib.ML
changeset 5537 c2bd39a2c0ee
parent 5143 b94cd208f073
child 6916 4957978b6f9e
--- a/src/HOL/ex/Fib.ML	Wed Sep 23 10:11:18 1998 +0200
+++ b/src/HOL/ex/Fib.ML	Wed Sep 23 10:12:01 1998 +0200
@@ -65,9 +65,9 @@
 				       mod_less, mod_Suc])));
 by (ALLGOALS
     (asm_full_simp_tac
-     (simpset() addsimps ([] @ add_ac @ mult_ac @
+     (simpset() addsimps add_ac @ mult_ac @
 			 [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
-			  mod_less, mod_Suc]))));
+			  mod_less, mod_Suc])));
 qed "fib_Cassini";