# HG changeset patch
# User blanchet
# Date 1392222959 -3600
# Node ID 3def821deb70ff21ac1cac8662064e03f3a6942d
# Parent  17fb554688f0dce45fdbd9f6e69fba3328ae3533
don't hide constant forever, since it may appear in some 'primcorec'-generated theorems

diff -r 17fb554688f0 -r 3def821deb70 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Feb 12 17:35:59 2014 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 12 17:35:59 2014 +0100
@@ -82,7 +82,7 @@
 apply (iprover elim: Nat_Abs_Nat_inverse [THEN subst])
 done
 
-wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]]
+wrap_free_constructors ["0 \<Colon> nat", Suc] case_nat [=] [[], [pred]] [[pred: "0 \<Colon> nat"]]
   apply atomize_elim
   apply (rename_tac n, induct_tac n rule: nat_induct0, auto)
  apply (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI
@@ -121,7 +121,7 @@
 
 declare nat.sel[code del]
 
-hide_const Nat.pred -- {* hide everything related to the selector *}
+hide_const (open) Nat.pred -- {* hide everything related to the selector *}
 hide_fact
   nat.case_eq_if
   nat.collapse