# HG changeset patch
# User haftmann
# Date 1495715921 -7200
# Node ID b6d458915f1bd69336293bb86bd4fc000b0cfccd
# Parent  b873cefb3b6a5ffd991c898a5fa7f13d5c4c007d
obsolete special case

diff -r b873cefb3b6a -r b6d458915f1b src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed May 24 16:35:18 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu May 25 14:38:41 2017 +0200
@@ -55,20 +55,6 @@
   or implemented for RBT trees.
 *)
 
-export_code _ checking SML OCaml? Haskell?
-
-(* Extra setup to make Scala happy *)
-(* If the compilation fails with an error "ambiguous implicit values",
-   read \<section>7.1 in the Code Generation Manual *)
-
-lemma [code]:
-  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
-unfolding gfp_def by blast
-
-lemma [code]:
-  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
-unfolding lfp_def by blast
-
-export_code _ checking Scala?
+export_code _ checking SML OCaml? Haskell? Scala
 
 end