# HG changeset patch # User wenzelm # Date 1208278156 -7200 # Node ID 0206185514687339edff8cfadb088ec9502ec0cf # Parent 39483503705fea48804a7857e62c02aee6796044 PureThy.hide_fact; diff -r 39483503705f -r 020618551468 src/HOL/Nominal/nominal_package.ML --- 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 **) 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 **)