# HG changeset patch
# User krauss
# Date 1257197040 -3600
# Node ID 9c6980f2eb39d23e6c2d98087cbed6e3b21ed298
# Parent  2240b0e7fa101ba2ea4c631205daa5e0fe357e45
conceal "termination" rule, used only by special tools

diff -r 2240b0e7fa10 -r 9c6980f2eb39 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Nov 02 22:23:57 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Mon Nov 02 22:24:00 2009 +0100
@@ -44,8 +44,8 @@
     [Simplifier.simp_add,
      Nitpick_Psimps.add]
 
-fun note_theorem ((name, atts), ths) =
-  LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
+fun note_theorem ((binding, atts), ths) =
+  LocalTheory.note Thm.generatedK ((binding, atts), ths)
 
 fun mk_defname fixes = fixes |> map (fst o fst) |> space_implode "_"
 
@@ -62,7 +62,8 @@
       val simps_by_f = sort saved_simps
 
       fun add_for_f fname simps =
-        note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
+        note_theorem ((Binding.qualified_name (Long_Name.qualify fname label), []), simps)
+        #> snd
     in
       (saved_simps,
        fold2 add_for_f fnames simps_by_f lthy)
@@ -89,7 +90,9 @@
           cont (Thm.close_derivation proof)
 
           val fnames = map (fst o fst) fixes
-          val qualify = Long_Name.qualify defname
+          fun qualify n = Binding.name n
+            |> Binding.qualify true defname
+
           val addsmps = add_simps fnames post sort_cont
 
           val (((psimps', pinducts'), (_, [termination'])), lthy) =
@@ -101,7 +104,7 @@
                    [Attrib.internal (K (Rule_Cases.case_names cnames)),
                     Attrib.internal (K (Rule_Cases.consumes 1)),
                     Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
-            ||>> note_theorem ((qualify "termination", []), [termination])
+            ||>> note_theorem ((Binding.conceal (qualify "termination"), []), [termination])
             ||> (snd o note_theorem ((qualify "cases",
                    [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
             ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros
@@ -147,7 +150,8 @@
               full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
             val tsimps = map remove_domain_condition psimps
             val tinduct = map remove_domain_condition pinducts
-            val qualify = Long_Name.qualify defname;
+            fun qualify n = Binding.name n
+              |> Binding.qualify true defname
           in
             lthy
             |> add_simps I "simps" simp_attribs tsimps |> snd