# HG changeset patch
# User haftmann
# Date 1496671185 -7200
# Node ID 2f45f4abf0a96cdd386a699c91cf719c9284a503
# Parent  03002d10bf1dd5acfdbe6fbb7cd46c6c06a0fb18
avoid duplicate

diff -r 03002d10bf1d -r 2f45f4abf0a9 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Mon Jun 05 15:59:45 2017 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Mon Jun 05 15:59:45 2017 +0200
@@ -8,6 +8,7 @@
   Complex_Main
   "~~/src/HOL/Library/Library"
   "~~/src/HOL/Library/Subseq_Order"
+  "~~/src/HOL/Library/RBT"
   "~~/src/HOL/Data_Structures/Tree_Map"
   "~~/src/HOL/Data_Structures/Tree_Set"
   "~~/src/HOL/Computational_Algebra/Computational_Algebra"
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.