--- 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"
--- 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.