diff -r ef02c5e051e5 -r e02bdf853a4c src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy --- a/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Thu Jan 10 12:07:05 2019 +0000 +++ b/src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy Thu Jan 10 12:07:08 2019 +0000 @@ -133,8 +133,6 @@ where "products A B = {c. \a b. a \ A \ b \ B \ c = a * b}" -export_code products in Haskell - -export_code union common_subsets products in Haskell +export_code union common_subsets products checking SML end