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 \We can export code:\ -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 \Using transfer with type \fset\\