--- a/thys/ReStar.thy	Tue Mar 08 05:03:47 2016 +0000
+++ b/thys/ReStar.thy	Tue Mar 08 06:30:48 2016 +0000
@@ -804,29 +804,27 @@
   "F_LEFT f v = Left (f v)"
 
 fun F_ALT where
-  "F_ALT f1 f2 (Right v) = Right (f2 v)"
-| "F_ALT f1 f2 (Left v) = Left (f1 v)" 
+  "F_ALT f\<^sub>1 f\<^sub>2 (Right v) = Right (f\<^sub>2 v)"
+| "F_ALT f\<^sub>1 f\<^sub>2 (Left v) = Left (f\<^sub>1 v)" 
 
 fun F_SEQ1 where
-  "F_SEQ1 f1 f2 v = Seq (f1 Void) (f2 v)"
+  "F_SEQ1 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 Void) (f\<^sub>2 v)"
 
 fun F_SEQ2 where 
-  "F_SEQ2 f1 f2 v = Seq (f1 v) (f2 Void)"
+  "F_SEQ2 f\<^sub>1 f\<^sub>2 v = Seq (f\<^sub>1 v) (f\<^sub>2 Void)"
 
 fun F_SEQ where 
-  "F_SEQ f1 f2 (Seq v1 v2) = Seq (f1 v1) (f2 v2)"
+  "F_SEQ f\<^sub>1 f\<^sub>2 (Seq v\<^sub>1 v\<^sub>2) = Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"
 
 fun simp_ALT where
-  "simp_ALT (ZERO, _) (r2, f2) = (r2, F_RIGHT f2)"
-| "simp_ALT (r1, f1) (ZERO, _) = (r1, F_LEFT f1)"
-| "simp_ALT (r1, f1) (r2, f2) = (ALT r1 r2, F_ALT f1 f2)"
+  "simp_ALT (ZERO, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_RIGHT f\<^sub>2)"
+| "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, f\<^sub>2) = (r\<^sub>1, F_LEFT f\<^sub>1)"
+| "simp_ALT (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (ALT r\<^sub>1 r\<^sub>2, F_ALT f\<^sub>1 f\<^sub>2)"
 
 fun simp_SEQ where
-  "simp_SEQ (ONE, f1) (r2, f2) = (r2, F_SEQ1 f1 f2)"
-| "simp_SEQ (r1, f1) (ONE, f2) = (r1, F_SEQ2 f1 f2)"
-| "simp_SEQ (ZERO, f1) (r2, f2) = (ZERO, f1)"
-| "simp_SEQ (r1, f1) (ZERO, f2) = (ZERO, f2)"
-| "simp_SEQ (r1, f1) (r2, f2) = (SEQ r1 r2, F_SEQ f1 f2)"  
+  "simp_SEQ (ONE, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (r\<^sub>2, F_SEQ1 f\<^sub>1 f\<^sub>2)"
+| "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"
+| "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"  
  
 fun 
   simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"