src/HOL/Bali/Value.thy
changeset 41778 5f79a9e42507
parent 37956 ee939247b2fb
child 58249 180f1b3508ed
--- a/src/HOL/Bali/Value.thy	Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Value.thy	Fri Feb 18 16:36:42 2011 +0100
@@ -26,7 +26,7 @@
 primrec the_Addr :: "val \<Rightarrow> loc"
   where "the_Addr (Addr a) = a"
 
-types   dyn_ty      = "loc \<Rightarrow> ty option"
+type_synonym dyn_ty = "loc \<Rightarrow> ty option"
 
 primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
 where