diff -r 3dd426ae6bea -r e87feee00a4c src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Wed Oct 19 23:07:48 2011 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Thu Oct 20 09:48:00 2011 +0200
@@ -10,7 +10,7 @@
 
 text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
 
-datatype 'a st = FunDom "name \<Rightarrow> 'a" "name list"
+datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
 
 fun "fun" where "fun (FunDom f _) = f"
 fun dom where "dom (FunDom _ A) = A"