src/HOL/Quotient_Examples/Lift_FSet.thy

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed May 16 19:15:45 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed May 16 19:17:20 2012 +0200
@@ -81,6 +81,10 @@
     done
 qed
 
+text {* We can export code: *}
+
+export_code fnil fcons fappend fmap ffilter fset in SML
+
 text {* Note that the generated transfer rule contains a composition
   of relations. The transfer rule is not yet very useful in this form. *}