diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -132,29 +132,29 @@
   for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
 begin
 
-abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
-where "\<gamma>\<^isub>s == \<gamma>_st \<gamma>"
+abbreviation \<gamma>\<^sub>s :: "'av st \<Rightarrow> state set"
+where "\<gamma>\<^sub>s == \<gamma>_st \<gamma>"
 
-abbreviation \<gamma>\<^isub>o :: "'av st option \<Rightarrow> state set"
-where "\<gamma>\<^isub>o == \<gamma>_option \<gamma>\<^isub>s"
+abbreviation \<gamma>\<^sub>o :: "'av st option \<Rightarrow> state set"
+where "\<gamma>\<^sub>o == \<gamma>_option \<gamma>\<^sub>s"
 
-abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
-where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
+abbreviation \<gamma>\<^sub>c :: "'av st option acom \<Rightarrow> state set acom"
+where "\<gamma>\<^sub>c == map_acom \<gamma>\<^sub>o"
 
-lemma gamma_s_top[simp]: "\<gamma>\<^isub>s \<top> = UNIV"
+lemma gamma_s_top[simp]: "\<gamma>\<^sub>s \<top> = UNIV"
 by(auto simp: \<gamma>_st_def fun_top)
 
-lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o \<top> = UNIV"
+lemma gamma_o_Top[simp]: "\<gamma>\<^sub>o \<top> = UNIV"
 by (simp add: top_option_def)
 
-lemma mono_gamma_s: "f \<le> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
+lemma mono_gamma_s: "f \<le> g \<Longrightarrow> \<gamma>\<^sub>s f \<subseteq> \<gamma>\<^sub>s g"
 by(simp add:\<gamma>_st_def le_st_iff subset_iff) (metis mono_gamma subsetD)
 
 lemma mono_gamma_o:
-  "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
+  "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^sub>o S1 \<subseteq> \<gamma>\<^sub>o S2"
 by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
 
-lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
+lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^sub>c C1 \<le> \<gamma>\<^sub>c C2"
 by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
 
 lemma in_gamma_option_iff: