src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
changeset 59484 a130ae7a9398
parent 58889 5b7a9633cfa8
child 59842 9fda99b3d5ee
     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu Feb 05 19:44:13 2015 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Thu Feb 05 19:44:14 2015 +0100
     1.3 @@ -11,6 +11,14 @@
     1.4    "~~/src/HOL/Library/RBT_Set"
     1.5  begin
     1.6  
     1.7 +setup \<open>
     1.8 +let
     1.9 +  val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
    1.10 +  val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
    1.11 +    @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
    1.12 +in fold Code.del_eqns consts end
    1.13 +\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    1.14 +
    1.15  (* 
    1.16     The following code equations have to be deleted because they use 
    1.17     lists to implement sets in the code generetor.