diff -r 8bef44f9b237 -r ee29edc644e8 Subst/UTLemmas.ML
--- a/Subst/UTLemmas.ML	Mon Aug 22 11:02:35 1994 +0200
+++ b/Subst/UTLemmas.ML	Mon Aug 22 11:54:23 1994 +0200
@@ -1,8 +1,8 @@
-(*  Title: 	Substitutions/utermlemmas.ML
+(*  Title: 	Substitutions/UTLemmas.ML
     Author: 	Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For utermlemmas.thy.  
+For UTLemmas.thy.  
 *)
 
 open UTLemmas;
@@ -22,7 +22,7 @@
        "t <: Comb(u,v) = (t=u | t=v | t <: u | t <: v)"];
 end;
 
-val utlemmas_ss = pair_ss addsimps (setplus_rews @ uterm_rews @ utlemmas_rews);
+val utlemmas_ss = prod_ss addsimps (setplus_rews @ uterm_rews @ utlemmas_rews);
 
 (****  occs irrefl ****)