--- a/thys/Sulzmann.thy	Fri Jun 24 12:35:16 2016 +0100
+++ b/thys/Sulzmann.thy	Wed Jul 20 14:30:07 2016 +0100
@@ -1,6 +1,6 @@
    
 theory Sulzmann
-  imports "Lexer" 
+  imports "Lexer" "~~/src/HOL/Library/Multiset"
 begin
 
 
@@ -82,6 +82,10 @@
                                     in (Stars_add v vs, ds''))"
 by pat_completeness auto
 
+termination
+apply(size_change)
+oops
+
 term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))"
 
 lemma decode'_smaller: