tuned

--- a/src/HOL/IMP/Abs_State.thy	Thu Apr 18 21:31:24 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Fri Apr 19 12:04:57 2013 +0200
@@ -17,6 +17,8 @@
 definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
 
+hide_type st  --"hide previous def to avoid long names"
+
 quotient_type 'a st = "('a::top) st_rep" / eq_st
 by (metis eq_st_def equivpI reflpI sympI transpI)