
diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Poly_Types.thy
--- a/src/HOL/IMP/Poly_Types.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Poly_Types.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -6,7 +6,7 @@
 
 text{* Everything else remains the same. *}
 
-type_synonym tyenv = "name \<Rightarrow> ty"
+type_synonym tyenv = "vname \<Rightarrow> ty"
 
 inductive atyping :: "tyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"
   ("(1_/ \<turnstile>p/ (_ :/ _))" [50,0,50] 50)




