--- a/src/HOL/Induct/SList.thy Sun Dec 27 21:46:36 2015 +0100
+++ b/src/HOL/Induct/SList.thy Sun Dec 27 22:07:17 2015 +0100
@@ -10,8 +10,8 @@
Definition of type 'a list (strict lists) by a least fixed point
-We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
-and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
+We use list(A) == lfp(%Z. {NUMB(0)} <+> A \<times> Z)
+and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) \<times> Z)
so that list can serve as a "functor" for defining other recursive types.