diff -r 2551ac44150e -r 9fda99b3d5ee src/HOL/Codegenerator_Test/Candidates.thy --- 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 \ +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 \ -- \drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\ inductive sublist :: "'a list \ 'a list \ bool"