# HG changeset patch
# User krauss
# Date 1257197043 -3600
# Node ID 62571cb5481159fd0fb167aed5a70fb61436db98
# Parent  9c6980f2eb39d23e6c2d98087cbed6e3b21ed298
conceal partial rules depending on config flag (i.e. when called via "fun")

diff -r 9c6980f2eb39 -r 62571cb54811 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Nov 02 22:24:00 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Mon Nov 02 22:24:03 2009 +0100
@@ -49,7 +49,7 @@
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
-fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
+fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy =
     let
       val spec = post simps
                    |> map (apfst (apsnd (fn ats => moreatts @ ats)))
@@ -62,7 +62,7 @@
       val simps_by_f = sort saved_simps
 
       fun add_for_f fname simps =
-        note_theorem ((Binding.qualified_name (Long_Name.qualify fname label), []), simps)
+        note_theorem ((mod_binding (Binding.qualify true fname (Binding.name label)), []), simps)
         #> snd
     in
       (saved_simps,
@@ -92,15 +92,16 @@
           val fnames = map (fst o fst) fixes
           fun qualify n = Binding.name n
             |> Binding.qualify true defname
+          val conceal_partial = if partials then I else Binding.conceal
 
           val addsmps = add_simps fnames post sort_cont
 
           val (((psimps', pinducts'), (_, [termination'])), lthy) =
             lthy
-            |> addsmps (Binding.qualify false "partial") "psimps"
-                 psimp_attribs psimps
-            ||> fold_option (snd oo addsmps I "simps" simp_attribs) trsimps
-            ||>> note_theorem ((qualify "pinduct",
+            |> addsmps (conceal_partial o Binding.qualify false "partial")
+                 "psimps" conceal_partial psimp_attribs psimps
+            ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
+            ||>> note_theorem ((conceal_partial (qualify "pinduct"),
                    [Attrib.internal (K (Rule_Cases.case_names cnames)),
                     Attrib.internal (K (Rule_Cases.consumes 1)),
                     Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
@@ -154,7 +155,7 @@
               |> Binding.qualify true defname
           in
             lthy
-            |> add_simps I "simps" simp_attribs tsimps |> snd
+            |> add_simps I "simps" I simp_attribs tsimps |> snd
             |> note_theorem
                ((qualify "induct",
                  [Attrib.internal (K (Rule_Cases.case_names case_names))]),
diff -r 9c6980f2eb39 -r 62571cb54811 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Mon Nov 02 22:24:00 2009 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Mon Nov 02 22:24:03 2009 +0100
@@ -65,8 +65,9 @@
       defname : string,
 
       (* contains no logical entities: invariant under morphisms *)
-      add_simps : (binding -> binding) -> string -> Attrib.src list -> thm list 
-                  -> local_theory -> thm list * local_theory,
+      add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+        Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+
       case_names : string list,
 
       fs : term list,