diff -r d430a1b34928 -r c7f56322a84b src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Prod.ML	Thu Jan 08 11:21:45 1998 +0100
@@ -241,19 +241,21 @@
 goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
 by (rtac split 1);
 qed "prod_fun";
+Addsimps [prod_fun];
 
 goal Prod.thy 
     "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
 by (rtac ext 1);
 by (res_inst_tac [("p","x")] PairE 1);
-by (asm_simp_tac (simpset() addsimps [prod_fun,o_def]) 1);
+by (Asm_simp_tac 1);
 qed "prod_fun_compose";
 
 goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)";
 by (rtac ext 1);
 by (res_inst_tac [("p","z")] PairE 1);
-by (asm_simp_tac (simpset() addsimps [prod_fun]) 1);
+by (Asm_simp_tac 1);
 qed "prod_fun_ident";
+Addsimps [prod_fun_ident];
 
 val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
 by (rtac image_eqI 1);
@@ -271,6 +273,7 @@
 by (blast_tac (claset() addIs [prod_fun]) 1);
 qed "prod_fun_imageE";
 
+
 (*** Disjoint union of a family of sets - Sigma ***)
 
 qed_goalw "SigmaI" Prod.thy [Sigma_def]