tuned;
authorwenzelm
Sun Mar 29 19:32:27 2015 +0200 (2015-03-29)
changeset 598429fda99b3d5ee
parent 59841 2551ac44150e
child 59843 b640b5e6b023
tuned;
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
     1.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Sun Mar 29 19:24:07 2015 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Sun Mar 29 19:32:27 2015 +0200
     1.3 @@ -13,11 +13,12 @@
     1.4  begin
     1.5  
     1.6  setup \<open>
     1.7 +fn thy =>
     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 +  val tycos = Sign.logical_types thy;
    1.12 +  val consts = map_filter (try (curry (Axclass.param_of_inst thy)
    1.13      @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
    1.14 -in fold Code.del_eqns consts end
    1.15 +in fold Code.del_eqns consts thy end
    1.16  \<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    1.17  
    1.18  inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
     2.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Mar 29 19:24:07 2015 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Mar 29 19:32:27 2015 +0200
     2.3 @@ -12,11 +12,12 @@
     2.4  begin
     2.5  
     2.6  setup \<open>
     2.7 +fn thy =>
     2.8  let
     2.9 -  val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
    2.10 -  val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
    2.11 +  val tycos = Sign.logical_types thy;
    2.12 +  val consts = map_filter (try (curry (Axclass.param_of_inst thy)
    2.13      @{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
    2.14 -in fold Code.del_eqns consts end
    2.15 +in fold Code.del_eqns consts thy end
    2.16  \<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
    2.17  
    2.18  (*