diff -r 890b68e1e8b6 -r f9d1442c70f3 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Mon Mar 30 22:34:59 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML	Tue Mar 31 00:11:54 2015 +0200
@@ -107,20 +107,20 @@
         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 concealed_partial = if partials then I else Binding.concealed
 
         val addsmps = add_simps fnames post sort_cont
 
         val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) =
           lthy
-          |> addsmps (conceal_partial o Binding.qualify false "partial")
-               "psimps" conceal_partial psimp_attribs psimps
-          ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
+          |> addsmps (concealed_partial o Binding.qualify false "partial")
+               "psimps" concealed_partial psimp_attribs psimps
+          ||>> Local_Theory.notes [((concealed_partial (qualify "pinduct"), []),
                 simple_pinducts |> map (fn th => ([th],
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
                   Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
                   Attrib.internal (K (Induct.induct_pred ""))])))]
-          ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]))
+          ||>> (apfst snd o Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination]))
           ||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) (fnames ~~ map single cases) (* TODO: case names *)
           ||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ pelims)
           ||> (case domintros of NONE => I | SOME thms =>