--- a/src/HOL/Codegenerator_Test/Candidates.thy Sun Mar 29 19:24:07 2015 +0200
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Sun Mar 29 19:32:27 2015 +0200
@@ -13,11 +13,12 @@
begin
setup \<open>
+fn thy =>
let
- val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
- val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
+ 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 end
+in fold Code.del_eqns consts thy end
\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Sun Mar 29 19:24:07 2015 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Sun Mar 29 19:32:27 2015 +0200
@@ -12,11 +12,12 @@
begin
setup \<open>
+fn thy =>
let
- val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
- val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
+ 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 end
+in fold Code.del_eqns consts thy end
\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
(*