diff -r 39483503705f -r 020618551468 src/HOL/Tools/inductive_realizer.ML
--- 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 **)