--- a/src/HOL/Lattice/Orders.thy Thu Jul 01 16:54:42 2010 +0200
+++ b/src/HOL/Lattice/Orders.thy Thu Jul 01 16:54:44 2010 +0200
@@ -196,7 +196,7 @@
\emph{not} be linear in general.
*}
-instantiation * :: (leq, leq) leq
+instantiation prod :: (leq, leq) leq
begin
definition
@@ -214,7 +214,7 @@
"p \<sqsubseteq> q \<Longrightarrow> (fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> C) \<Longrightarrow> C"
by (unfold leq_prod_def) blast
-instance * :: (quasi_order, quasi_order) quasi_order
+instance prod :: (quasi_order, quasi_order) quasi_order
proof
fix p q r :: "'a::quasi_order \<times> 'b::quasi_order"
show "p \<sqsubseteq> p"
@@ -234,7 +234,7 @@
qed
qed
-instance * :: (partial_order, partial_order) partial_order
+instance prod :: (partial_order, partial_order) partial_order
proof
fix p q :: "'a::partial_order \<times> 'b::partial_order"
assume pq: "p \<sqsubseteq> q" and qp: "q \<sqsubseteq> p"