diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/Nominal/Examples/Class3.thy
--- a/src/HOL/Nominal/Examples/Class3.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Nominal/Examples/Class3.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -2265,7 +2265,7 @@
 by (induct rule: SNa.induct) (blast)
 
 lemma wf_SNa_restricted:
-  shows "wf (A_Redu_set \<inter> (UNIV <*> SNa_set))"
+  shows "wf (A_Redu_set \<inter> (UNIV \<times> SNa_set))"
 apply(unfold wf_def)
 apply(intro strip)
 apply(case_tac "SNa x")
@@ -2280,7 +2280,7 @@
 done
 
 definition SNa_Redu :: "(trm \<times> trm) set" where
-  "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV <*> SNa_set)"
+  "SNa_Redu \<equiv> A_Redu_set \<inter> (UNIV \<times> SNa_set)"
 
 lemma wf_SNa_Redu:
   shows "wf SNa_Redu"