
diff -r 7aaebfcf3134 -r 435fb018e8ee src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -113,7 +113,8 @@
 
 text \<open>We can export code:\<close>
 
-export_code fnil fcons fappend fmap ffilter fset fmember in SML
+export_code fnil fcons fappend fmap ffilter fset fmember in SML file_prefix fset
+
 
 subsection \<open>Using transfer with type \<open>fset\<close>\<close>
 




