doc-src/TutorialI/CodeGen/CodeGen.thy
changeset 42765 aec61b60ff7b
parent 27015 f8537d69f514
--- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Thu May 12 17:17:57 2011 +0200
@@ -15,7 +15,7 @@
 appropriate function itself.
 *}
 
-types 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
+type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v";
 datatype ('a,'v)expr = Cex 'v
                      | Vex 'a
                      | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";