# HG changeset patch
# User wenzelm
# Date 1441569313 -7200
# Node ID efe8b18306b7c0f89c420add457a3df0b4fabd86
# Parent  65082457c117bd77dde610eed59489739a028c70
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';

diff -r 65082457c117 -r efe8b18306b7 NEWS
--- a/NEWS	Sun Sep 06 19:09:20 2015 +0200
+++ b/NEWS	Sun Sep 06 21:55:13 2015 +0200
@@ -282,6 +282,11 @@
 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef'
 command. Minor INCOMPATIBILITY, use 'function' instead.
 
+* Recursive function definitions ('fun', 'function', 'partial_function')
+no longer expose the low-level "_def" facts of the internal
+construction. INCOMPATIBILITY, enable option "function_defs" in the
+context for rare situations where these facts are really needed.
+
 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
 
 
diff -r 65082457c117 -r efe8b18306b7 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Sun Sep 06 19:09:20 2015 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Sun Sep 06 21:55:13 2015 +0200
@@ -1757,9 +1757,9 @@
   compare.eq.refl compare.eq.simps
   compare.EQ_def compare.GT_def compare.LT_def
   equal_compare_def
-  skip_red_def skip_red.simps skip_red.cases skip_red.induct 
+  skip_red.simps skip_red.cases skip_red.induct 
   skip_black_def
-  compare_height_def compare_height.simps
+  compare_height.simps
 
 subsection \<open>union and intersection of sorted associative lists\<close>
 
diff -r 65082457c117 -r efe8b18306b7 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Sun Sep 06 19:09:20 2015 +0200
+++ b/src/HOL/Nitpick.thy	Sun Sep 06 21:55:13 2015 +0200
@@ -239,8 +239,8 @@
 
 hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold prod_def refl'_def wf'_def
   card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
-  size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
-  num_def denom_def norm_frac_def frac_def plus_frac_def times_frac_def uminus_frac_def
+  size_list_simp nat_lcm_def int_gcd_def int_lcm_def Frac_def zero_frac_def one_frac_def
+  num_def denom_def frac_def plus_frac_def times_frac_def uminus_frac_def
   number_of_frac_def inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
   wfrec'_def
 
diff -r 65082457c117 -r efe8b18306b7 src/HOL/Quickcheck_Exhaustive.thy
--- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Sep 06 19:09:20 2015 +0200
+++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Sep 06 21:55:13 2015 +0200
@@ -646,11 +646,6 @@
 hide_fact (open) orelse_def
 no_notation orelse (infixr "orelse" 55)
 
-hide_fact
-  exhaustive_int'_def
-  exhaustive_integer'_def
-  exhaustive_natural'_def
-
 hide_const valtermify_absdummy valtermify_fun_upd valterm_emptyset valtermify_insert valtermify_pair
   valtermify_Inl valtermify_Inr
   termify_fun_upd term_emptyset termify_insert termify_pair setify
diff -r 65082457c117 -r efe8b18306b7 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Sep 06 19:09:20 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Sep 06 21:55:13 2015 +0200
@@ -7,7 +7,6 @@
 signature FUNCTION_CORE =
 sig
   val trace: bool Unsynchronized.ref
-
   val prepare_function : Function_Common.function_config
     -> string (* defname *)
     -> ((bstring * typ) * mixfix) list (* defined symbol *)
@@ -504,10 +503,12 @@
       Abs ("x", domT, Const (@{const_name Fun_Def.THE_default}, ranT --> (ranT --> boolT) --> ranT)
         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
       |> Syntax.check_term lthy
+    val def_binding =
+      if Config.get lthy function_defs then (Binding.name fdefname, [])
+      else Attrib.empty_binding
   in
     Local_Theory.define
-      ((Binding.name (function_name fname), mixfix),
-        ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy
+      ((Binding.name (function_name fname), mixfix), (def_binding, f_def)) lthy
   end
 
 fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
diff -r 65082457c117 -r efe8b18306b7 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Sun Sep 06 19:09:20 2015 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Sun Sep 06 21:55:13 2015 +0200
@@ -7,6 +7,8 @@
 
 signature FUNCTION_LIB =
 sig
+  val function_defs: bool Config.T
+
   val plural: string -> string -> 'a list -> string
 
   val dest_all_all: term -> term list * term
@@ -30,6 +32,9 @@
 structure Function_Lib: FUNCTION_LIB =
 struct
 
+val function_defs = Attrib.setup_config_bool @{binding function_defs} (K false)
+
+
 (* "The variable" ^ plural " is" "s are" vs *)
 fun plural sg pl [x] = sg
   | plural sg pl _ = pl
diff -r 65082457c117 -r efe8b18306b7 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun Sep 06 19:09:20 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun Sep 06 21:55:13 2015 +0200
@@ -128,11 +128,13 @@
   let
     fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
       let
+        val def_binding =
+          if Config.get lthy function_defs then (Binding.name (Thm.def_name fname), [])
+          else Attrib.empty_binding
         val ((f, (_, f_defthm)), lthy') =
           Local_Theory.define
             ((Binding.name fname, mixfix),
-              ((Binding.concealed (Binding.name (Thm.def_name fname)), []),
-              Term.subst_bound (fsum, f_def))) lthy
+              (def_binding, Term.subst_bound (fsum, f_def))) lthy
       in
         (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
            f=SOME f, f_defthm=SOME f_defthm },
diff -r 65082457c117 -r efe8b18306b7 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Sun Sep 06 19:09:20 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Sun Sep 06 21:55:13 2015 +0200
@@ -258,9 +258,11 @@
     val inst_mono_thm = Thm.forall_elim (Thm.cterm_of lthy x_uc) mono_thm
 
     val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
-    val f_def_binding = Binding.concealed (Binding.name (Thm.def_name fname));
+    val f_def_binding =
+      if Config.get lthy Function_Lib.function_defs then (Binding.name (Thm.def_name fname), [])
+      else Attrib.empty_binding;
     val ((f, (_, f_def)), lthy') = Local_Theory.define
-      ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy;
+      ((f_binding, mixfix), (f_def_binding, f_def_rhs)) lthy;
 
     val eqn = HOLogic.mk_eq (list_comb (f, args),
         Term.betapplys (F, f :: args))