changeset 42107 | a6725f293377 |
parent 42098 | f978caf60bbe |
child 42352 | 69221145175d |
--- a/src/HOL/Tools/Metis/metis_translate.ML Thu Mar 24 17:49:27 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Thu Mar 24 17:49:27 2011 +0100 @@ -805,7 +805,7 @@ val helper_ths = metis_helpers |> filter (is_used o fst) - |> maps (fn (c, (needs_full_types, thms)) => + |> maps (fn (_, (needs_full_types, thms)) => if needs_full_types andalso mode <> FT then [] else map prepare_helper thms) in lmap |> fold (add_thm false) helper_ths end