--- a/thys3/Blexer.thy	Mon Aug 22 17:58:29 2022 +0100
+++ b/thys3/Blexer.thy	Tue Aug 23 14:21:13 2022 +0100
@@ -264,6 +264,13 @@
   apply(simp_all)
   done
 
+lemma retrieve_codestars2:
+  assumes "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v"
+  shows "retrieve (ASTAR bs (intern r)) (Stars []) = bs @ [S]"
+  apply simp
+  done
+
+
 lemma retrieve_fuse2:
   assumes "\<Turnstile> v : (erase r)"
   shows "retrieve (fuse bs r) v = bs @ retrieve r v"