src/HOL/MicroJava/DFA/LBVSpec.thy

--- a/src/HOL/MicroJava/DFA/LBVSpec.thy	Fri Apr 22 15:57:43 2011 +0200
+++ b/src/HOL/MicroJava/DFA/LBVSpec.thy	Sat Apr 23 13:00:19 2011 +0200
@@ -9,8 +9,7 @@
 imports SemilatAlg Opt
 begin
 
-types
-  's certificate = "'s list"   
+type_synonym 's certificate = "'s list"   
 
 primrec merge :: "'s certificate \<Rightarrow> 's binop \<Rightarrow> 's ord \<Rightarrow> 's \<Rightarrow> nat \<Rightarrow> (nat \<times> 's) list \<Rightarrow> 's \<Rightarrow> 's" where
   "merge cert f r T pc []     x = x"