# HG changeset patch
# User paulson
# Date 953573051 -3600
# Node ID 6c48043ccd0edb50db4f6b6d5a391f2e54aba6bc
# Parent  ce6ae118b6b226a8b59cccf111f9e2d683a32ff8
the perm_rules variable is no longer needed

diff -r ce6ae118b6b2 -r 6c48043ccd0e src/HOL/ex/Factorization.ML
--- a/src/HOL/ex/Factorization.ML	Mon Mar 20 12:54:31 2000 +0100
+++ b/src/HOL/ex/Factorization.ML	Mon Mar 20 18:24:11 2000 +0100
@@ -133,7 +133,7 @@
 
 Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)";
 by (induct_tac "l" 1);
-by (ALLGOALS Asm_full_simp_tac);
+by Auto_tac;
 qed "oinsert_x_y";
 
 
@@ -146,24 +146,24 @@
 
 Goal "xs <~~> ys ==> prod xs = prod ys";
 by (etac perm.induct 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_left_commute])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac)));
 qed_spec_mp "perm_prod";
 
 Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"; 
 by (etac perm.induct 1);
-by (auto_tac (claset() addIs perm_rules, simpset()));
+by Auto_tac;
 qed "perm_subst_oinsert";
 
 Goal "x#xs <~~> oinsert x xs";
 by (induct_tac "xs" 1);
-by (auto_tac (claset() addIs perm_rules, simpset()));
+by Auto_tac;
 qed "perm_oinsert";
 
 Goal "xs <~~> sort xs";
 by (induct_tac "xs" 1);
-by (auto_tac (claset() addIs [perm.trans,perm_oinsert] 
+by (auto_tac (claset() addIs [perm_oinsert] 
 	               addEs [perm_subst_oinsert],
-              simpset() addsimps [perm_refl]));
+              simpset()));
 qed "perm_sort";
 
 Goal "xs <~~> ys ==> sort xs = sort ys";