--- a/PIPDefs.thy	Tue Jun 27 14:49:42 2017 +0100
+++ b/PIPDefs.thy	Thu Jun 29 14:59:55 2017 +0100
@@ -679,8 +679,8 @@
   "tG (s::state) \<equiv> tG_raw (wq s)"
 
 lemma tG_alt_def: 
-  "tG s = {(th1, th2) | th1 th2. 
-                  \<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}" (is "?L = ?R")
+  "tG s = {(th\<^sub>1, th\<^sub>2) | th\<^sub>1 th\<^sub>2. 
+                  \<exists> cs. (Th th\<^sub>1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th\<^sub>2) \<in> RAG s}" (is "?L = ?R")
   by (unfold s_tG_abv s_RAG_abv tG_raw_def, simp)
 
 lemma tRAG_def_tG: "tRAG s = (map_prod Th Th) ` (tG s)"