--- a/src/HOL/Nominal/nominal_package.ML Tue Apr 15 18:49:15 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Tue Apr 15 18:49:16 2008 +0200
@@ -1489,8 +1489,7 @@
(map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (("", []), x)) rec_intr_ts) [] ||>
- PureThy.hide_thms true [NameSpace.append
- (Sign.full_name thy10 big_rec_name) "induct"];
+ PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
(** equivariance **)