
diff -r 03002d10bf1d -r 2f45f4abf0a9 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jun 05 15:59:45 2017 +0200
@@ -11,15 +11,6 @@
   "~~/src/HOL/Library/RBT_Set"
 begin
 
-setup \<open>
-fn thy =>
-let
-  val tycos = Sign.logical_types thy;
-  val consts = map_filter (try (curry (Axclass.param_of_inst thy)
-    @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
-in fold Code.del_eqns consts thy end
-\<close> \<comment> \<open>drop technical stuff from \<open>Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>
-
 text \<open>
   The following code equations have to be deleted because they use 
   lists to implement sets in the code generetor. 




