1.1 --- a/NEWS	Sat Mar 17 15:33:08 2012 +0100
     1.2 +++ b/NEWS	Sat Mar 17 16:07:03 2012 +0100
     1.3 @@ -390,10 +390,13 @@
     1.4  header declaration; it can be passed to Outer_Syntax.command etc.
     1.5  
     1.6  * Local_Theory.define no longer hard-wires default theorem name
     1.7 -"foo_def": definitional packages need to make this explicit, and may
     1.8 -choose to omit theorem bindings for definitions by using
     1.9 -Binding.empty/Attrib.empty_binding.  Potential INCOMPATIBILITY for
    1.10 -derived definitional packages.
    1.11 +"foo_def", but retains the binding as given.  If that is Binding.empty
    1.12 +/ Attrib.empty_binding, the result is not registered as user-level
    1.13 +fact.  The Local_Theory.define_internal variant allows to specify a
    1.14 +non-empty name (used for the foundation in the background theory),
    1.15 +while omitting the fact binding in the user-context.  Potential
    1.16 +INCOMPATIBILITY for derived definitional packages: need to specify
    1.17 +naming policy for primitive definitions more explicitly.
    1.18  
    1.19  * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
    1.20  conformance with similar operations in structure Term and Logic.

     2.1 --- a/src/Pure/Isar/generic_target.ML	Sat Mar 17 15:33:08 2012 +0100
     2.2 +++ b/src/Pure/Isar/generic_target.ML	Sat Mar 17 16:07:03 2012 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  sig
     2.5    val define: (((binding * typ) * mixfix) * (binding * term) ->
     2.6        term list * term list -> local_theory -> (term * thm) * local_theory) ->
     2.7 -    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     2.8 +    bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     2.9      (term * (string * thm)) * local_theory
    2.10    val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
    2.11        (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
    2.12 @@ -48,7 +48,7 @@
    2.13  
    2.14  (* define *)
    2.15  
    2.16 -fun define foundation ((b, mx), ((b_def, atts), rhs)) lthy =
    2.17 +fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
    2.18    let
    2.19      val thy = Proof_Context.theory_of lthy;
    2.20      val thy_ctxt = Proof_Context.init_global thy;
    2.21 @@ -88,7 +88,8 @@
    2.22  
    2.23      (*note*)
    2.24      val ([(res_name, [res])], lthy4) = lthy3
    2.25 -      |> Local_Theory.notes_kind "" [((b_def, atts), [([def], [])])];
    2.26 +      |> Local_Theory.notes_kind ""
    2.27 +        [((if internal then Binding.empty else b_def, atts), [([def], [])])];
    2.28    in ((lhs, (res_name, res)), lthy4) end;
    2.29  
    2.30  

     3.1 --- a/src/Pure/Isar/local_theory.ML	Sat Mar 17 15:33:08 2012 +0100
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Mar 17 16:07:03 2012 +0100
     3.3 @@ -32,6 +32,8 @@
     3.4    val global_morphism: local_theory -> morphism
     3.5    val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     3.6      (term * (string * thm)) * local_theory
     3.7 +  val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     3.8 +    (term * (string * thm)) * local_theory
     3.9    val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
    3.10    val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
    3.11      local_theory -> (string * thm list) list * local_theory
    3.12 @@ -63,7 +65,7 @@
    3.13  (* type lthy *)
    3.14  
    3.15  type operations =
    3.16 - {define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    3.17 + {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    3.18      (term * (string * thm)) * local_theory,
    3.19    notes: string ->
    3.20      (Attrib.binding * (thm list * Attrib.src list) list) list ->
    3.21 @@ -195,7 +197,8 @@
    3.22  
    3.23  val pretty = operation #pretty;
    3.24  val abbrev = apsnd checkpoint ooo operation2 #abbrev;
    3.25 -val define = apsnd checkpoint oo operation1 #define;
    3.26 +val define = apsnd checkpoint oo operation2 #define false;
    3.27 +val define_internal = apsnd checkpoint oo operation2 #define true;
    3.28  val notes_kind = apsnd checkpoint ooo operation2 #notes;
    3.29  val declaration = checkpoint ooo operation2 #declaration;
    3.30  

     4.1 --- a/src/Pure/Isar/specification.ML	Sat Mar 17 15:33:08 2012 +0100
     4.2 +++ b/src/Pure/Isar/specification.ML	Sat Mar 17 16:07:03 2012 +0100
     4.3 @@ -214,7 +214,7 @@
     4.4            in (b, mx) end);
     4.5      val name = Thm.def_binding_optional b raw_name;
     4.6      val ((lhs, (_, raw_th)), lthy2) = lthy
     4.7 -      |> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs));
     4.8 +      |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));
     4.9  
    4.10      val th = prove lthy2 raw_th;
    4.11      val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);