Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PureThy.hide_fact;
authorwenzelm
Tue, 15 Apr 2008 18:49:16 +0200
changeset 26663 020618551468
parent 26662 39483503705f
child 26664 167d879a89b0
PureThy.hide_fact;
src/HOL/Nominal/nominal_package.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/inductive_realizer.ML file | annotate | diff | comparison | revisions 
--- 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 **)
 
--- 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 **)
isabelle