diff -r 7aaebfcf3134 -r 435fb018e8ee src/HOL/Quotient_Examples/Lift_DList.thy
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -50,5 +50,6 @@
 text \<open>We can export code:\<close>
 
 export_code empty insert remove map filter null member length fold foldr concat in SML
+  file_prefix dlist
 
 end