--- a/thys/Paper/Paper.thy	Fri Mar 11 00:56:46 2016 +0000
+++ b/thys/Paper/Paper.thy	Fri Mar 11 10:43:44 2016 +0000
@@ -36,14 +36,12 @@
   Sequ ("_ @ _" [78,77] 63) and
   injval ("inj _ _ _" [79,77,79] 76) and 
   mkeps ("mkeps _" [79] 76) and 
-  (*projval ("proj _ _ _" [1000,77,1000] 77) and*) 
   length ("len _" [78] 73) and
-  matcher ("lexer _ _" [78,78] 77) and
-
+ 
   Prf ("_ : _" [75,75] 75) and  
   PMatch ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
-  (* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *)
-  
+ 
+  lexer ("lexer _ _" [78,78] 77) and 
   F_RIGHT ("F\<^bsub>Right\<^esub> _") and
   F_LEFT ("F\<^bsub>Left\<^esub> _") and  
   F_ALT ("F\<^bsub>Alt\<^esub> _ _") and
@@ -52,7 +50,7 @@
   F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and
   simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and
   simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and
-  matcher3 ("lexer\<^sup>+ _ _" [78,78] 77)
+  slexer ("lexer\<^sup>+ _ _" [78,78] 77)
 
 definition 
   "match r s \<equiv> nullable (ders s r)"
@@ -558,8 +556,8 @@
 
   \begin{center}
   \begin{tabular}{lcl}
-  @{thm (lhs) matcher.simps(1)} & $\dn$ & @{thm (rhs) matcher.simps(1)}\\
-  @{thm (lhs) matcher.simps(2)} & $\dn$ & @{text "case"} @{term "matcher (der c r) s"} @{text of}\\
+  @{thm (lhs) lexer.simps(1)} & $\dn$ & @{thm (rhs) lexer.simps(1)}\\
+  @{thm (lhs) lexer.simps(2)} & $\dn$ & @{text "case"} @{term "lexer (der c r) s"} @{text of}\\
                      & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\
                      & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{term "Some (injval r c v)"}                          
   \end{tabular}
@@ -870,10 +868,10 @@
   
   \begin{center}
   \begin{tabular}{lcl}
-  @{thm (lhs) matcher3.simps(1)} & $\dn$ & @{thm (rhs) matcher3.simps(1)}\\
-  @{thm (lhs) matcher3.simps(2)} & $\dn$ & 
+  @{thm (lhs) slexer.simps(1)} & $\dn$ & @{thm (rhs) slexer.simps(1)}\\
+  @{thm (lhs) slexer.simps(2)} & $\dn$ & 
                          @{text "let (r\<^sub>s, f\<^sub>r) = simp (r "}$\backslash$@{text " c) in"}\\
-                     & & @{text "case"} @{term "matcher3 r\<^sub>s s"} @{text of}\\
+                     & & @{text "case"} @{term "slexer r\<^sub>s s"} @{text of}\\
                      & & \phantom{$|$} @{term "None"}  @{text "\<Rightarrow>"} @{term None}\\
                      & & $|$ @{term "Some v"} @{text "\<Rightarrow>"} @{text "Some (inj r c (f\<^sub>r v))"}                          
   \end{tabular}
@@ -888,7 +886,7 @@
   it (that is construct @{term "f\<^sub>r v"}). We can prove that
 
   \begin{lemma}
-  @{term "matcher3 r s = matcher r s"}
+  @{term "slexer r s = lexer r s"}
   \end{lemma}
 
   \noindent