PureThy.hide_fact;
authorwenzelm
Tue Apr 15 18:49:16 2008 +0200 (2008-04-15)
changeset 26663020618551468
parent 26662 39483503705f
child 26664 167d879a89b0
PureThy.hide_fact;
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Apr 15 18:49:15 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Apr 15 18:49:16 2008 +0200
     1.3 @@ -1489,8 +1489,7 @@
     1.4            (map (fn (s, T) => ((s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
     1.5            (map dest_Free rec_fns)
     1.6            (map (fn x => (("", []), x)) rec_intr_ts) [] ||>
     1.7 -      PureThy.hide_thms true [NameSpace.append
     1.8 -        (Sign.full_name thy10 big_rec_name) "induct"];
     1.9 +      PureThy.hide_fact true (NameSpace.append (Sign.full_name thy10 big_rec_name) "induct");
    1.10  
    1.11      (** equivariance **)
    1.12  
     2.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Apr 15 18:49:15 2008 +0200
     2.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Apr 15 18:49:16 2008 +0200
     2.3 @@ -359,8 +359,7 @@
     2.4             subst_atomic rlzpreds' (Logic.unvarify rintr)))
     2.5               (rintrs ~~ maps snd rss)) [] ||>
     2.6        Sign.absolute_path;
     2.7 -    val thy3 = PureThy.hide_thms false
     2.8 -      (map name_of_thm (#intrs ind_info)) thy3';
     2.9 +    val thy3 = fold (PureThy.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
    2.10  
    2.11      (** realizer for induction rule **)
    2.12