no longer declare .psimps rules as [simp].

This regularly caused confusion (e.g., they show up in simp traces
when the regular simp rules are disabled). In the few places where the
rules are used, explicitly mentioning them actually clarifies the
proof text.

--- a/NEWS	Tue Sep 28 09:43:13 2010 +0200
+++ b/NEWS	Tue Sep 28 09:54:07 2010 +0200
@@ -236,6 +236,9 @@
 generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
 The theorems bij_def and surj_def are unchanged.
 
+* Function package: .psimps rules are no longer implicitly declared [simp].
+INCOMPATIBILITY.
+
 *** FOL ***
 
 * All constant names are now qualified.  INCOMPATIBILITY.

--- a/doc-src/Functions/Thy/Functions.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/doc-src/Functions/Thy/Functions.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -763,11 +763,10 @@
   \noindent The hypothesis in our lemma was used to satisfy the first premise in
   the induction rule. However, we also get @{term
   "findzero_dom (f, n)"} as a local assumption in the induction step. This
-  allows to unfold @{term "findzero f n"} using the @{text psimps}
-  rule, and the rest is trivial. Since the @{text psimps} rules carry the
-  @{text "[simp]"} attribute by default, we just need a single step:
+  allows unfolding @{term "findzero f n"} using the @{text psimps}
+  rule, and the rest is trivial.
  *}
-apply simp
+apply (simp add: findzero.psimps)
 done
 
 text {*
@@ -794,7 +793,7 @@
   have "f n \<noteq> 0"
   proof 
     assume "f n = 0"
-    with dom have "findzero f n = n" by simp
+    with dom have "findzero f n = n" by (simp add: findzero.psimps)
     with x_range show False by auto
   qed
   
@@ -805,7 +804,7 @@
     with `f n \<noteq> 0` show ?thesis by simp
   next
     assume "x \<in> {Suc n ..< findzero f n}"
-    with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp
+    with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by (simp add: findzero.psimps)
     with IH and `f n \<noteq> 0`
     show ?thesis by simp
   qed
@@ -1069,7 +1068,7 @@
 *}
 (*<*)oops(*>*)
 lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"
-  by (induct rule:nz.pinduct) auto
+  by (induct rule:nz.pinduct) (auto simp: nz.psimps)
 
 text {*
   We formulate this as a partial correctness lemma with the condition
@@ -1105,7 +1104,7 @@
 lemma f91_estimate: 
   assumes trm: "f91_dom n" 
   shows "n < f91 n + 11"
-using trm by induct auto
+using trm by induct (auto simp: f91.psimps)
 
 termination
 proof

--- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -54,7 +54,7 @@
            | None \<Rightarrow> None)
    | None \<Rightarrow> None
    )"
-apply (cases "mrec_dom (x,h)", simp)
+apply (cases "mrec_dom (x,h)", simp add: mrec.psimps)
 apply (frule mrec_default)
 apply (frule mrec_di_reverse, simp)
 by (auto split: sum.split option.split simp: mrec_default)
@@ -105,7 +105,7 @@
       proof (cases a)
         case (Inl aa)
         from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
-          by auto
+          by (auto simp: mrec.psimps)
       next
         case (Inr b)
         note Inr' = this
@@ -122,15 +122,15 @@
             apply auto
             apply (rule rec_case)
             apply auto
-            unfolding MREC_def by auto
+            unfolding MREC_def by (auto simp: mrec.psimps)
         next
           case None
-          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
+          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps)
         qed
       qed
     next
       case None
-      from this 1(1) mrec 1(3) show ?thesis by simp
+      from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps)
     qed
   qed
   from this h'_r show ?thesis by simp

--- a/src/HOL/Tools/Function/function.ML	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/Tools/Function/function.ML	Tue Sep 28 09:54:07 2010 +0200
@@ -52,8 +52,7 @@
    Nitpick_Simps.add]
 
 val psimp_attribs = map (Attrib.internal o K)
-  [Simplifier.simp_add,
-   Nitpick_Psimps.add]
+  [Nitpick_Psimps.add]
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 

--- a/src/HOL/ex/Fundefs.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -51,7 +51,7 @@
   assumes trm: "nz_dom x"
   shows "nz x = 0"
 using trm
-by induct auto
+by induct (auto simp: nz.psimps)
 
 termination nz
   by (relation "less_than") (auto simp:nz_is_zero)
@@ -71,7 +71,7 @@
 lemma f91_estimate: 
   assumes trm: "f91_dom n"
   shows "n < f91 n + 11"
-using trm by induct auto
+using trm by induct (auto simp: f91.psimps)
 
 termination
 proof

--- a/src/HOL/ex/Unification.thy	Tue Sep 28 09:43:13 2010 +0200
+++ b/src/HOL/ex/Unification.thy	Tue Sep 28 09:54:07 2010 +0200
@@ -158,6 +158,7 @@
                                          Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
   by pat_completeness auto
 
+declare unify.psimps[simp]
 
 subsection {* Partial correctness *}
 
@@ -533,4 +534,6 @@
   qed
 qed
 
+declare unify.psimps[simp del]
+
 end