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