diff -r f02b26f7d39d -r 7fba644ed827 src/HOL/BNF_Wellorder_Constructions.thy
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Sun Dec 27 22:07:17 2015 +0100
@@ -1515,19 +1515,19 @@
 "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
 
 lemma curr_in:
-assumes f: "f \<in> Func (A <*> B) C"
+assumes f: "f \<in> Func (A \<times> B) C"
 shows "curr A f \<in> Func A (Func B C)"
 using assms unfolding curr_def Func_def by auto
 
 lemma curr_inj:
-assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
+assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
 shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
 proof safe
   assume c: "curr A f1 = curr A f2"
   show "f1 = f2"
   proof (rule ext, clarify)
     fix a b show "f1 (a, b) = f2 (a, b)"
-    proof (cases "(a,b) \<in> A <*> B")
+    proof (cases "(a,b) \<in> A \<times> B")
       case False
       thus ?thesis using assms unfolding Func_def by auto
     next
@@ -1540,7 +1540,7 @@
 
 lemma curr_surj:
 assumes "g \<in> Func A (Func B C)"
-shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
+shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
 proof
   let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
   show "curr A ?f = g"
@@ -1557,11 +1557,11 @@
       thus ?thesis using True unfolding Func_def curr_def by auto
     qed
   qed
-  show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
+  show "?f \<in> Func (A \<times> B) C" using assms unfolding Func_def mem_Collect_eq by auto
 qed
 
 lemma bij_betw_curr:
-"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
+"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
 unfolding bij_betw_def inj_on_def image_def
 apply (intro impI conjI ballI)
 apply (erule curr_inj[THEN iffD1], assumption+)