diff -r c7be23634728 -r 6d4c3ee8219d src/HOL/Hahn_Banach/Function_Order.thy
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Tue Feb 22 16:47:18 2011 +0100
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Tue Feb 22 17:06:14 2011 +0100
@@ -21,7 +21,7 @@
   graph.
 *}
 
-types 'a graph = "('a \<times> real) set"
+type_synonym 'a graph = "('a \<times> real) set"
 
 definition
   graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where