src/HOL/Quotient_Examples/Lift_FSet.thy
changeset 70009 435fb018e8ee
parent 67399 eab6ce8368fa
child 80768 c7723cc15de8
--- 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>