changeset 26663 | 020618551468 |
parent 26626 | c6231d64d264 |
child 26711 | 3a478bfa1650 |
--- a/src/HOL/Tools/inductive_realizer.ML Tue Apr 15 18:49:15 2008 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Apr 15 18:49:16 2008 +0200 @@ -359,8 +359,7 @@ subst_atomic rlzpreds' (Logic.unvarify rintr))) (rintrs ~~ maps snd rss)) [] ||> Sign.absolute_path; - val thy3 = PureThy.hide_thms false - (map name_of_thm (#intrs ind_info)) thy3'; + val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3'; (** realizer for induction rule **)