--- 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 ****)