# HG changeset patch
# User wenzelm
# Date 1331996823 -3600
# Node ID eeea81b86b70516f9a641230e128b87591d5e758
# Parent  196f2d9406c4d0d3782640cb2b79258c0c1766f1
refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.;
actually make "raw_def" internal (cf. 80123a220219);

diff -r 196f2d9406c4 -r eeea81b86b70 NEWS
--- a/NEWS	Sat Mar 17 15:33:08 2012 +0100
+++ b/NEWS	Sat Mar 17 16:07:03 2012 +0100
@@ -390,10 +390,13 @@
 header declaration; it can be passed to Outer_Syntax.command etc.
 
 * Local_Theory.define no longer hard-wires default theorem name
-"foo_def": definitional packages need to make this explicit, and may
-choose to omit theorem bindings for definitions by using
-Binding.empty/Attrib.empty_binding.  Potential INCOMPATIBILITY for
-derived definitional packages.
+"foo_def", but retains the binding as given.  If that is Binding.empty
+/ Attrib.empty_binding, the result is not registered as user-level
+fact.  The Local_Theory.define_internal variant allows to specify a
+non-empty name (used for the foundation in the background theory),
+while omitting the fact binding in the user-context.  Potential
+INCOMPATIBILITY for derived definitional packages: need to specify
+naming policy for primitive definitions more explicitly.
 
 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
 conformance with similar operations in structure Term and Logic.
diff -r 196f2d9406c4 -r eeea81b86b70 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat Mar 17 15:33:08 2012 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sat Mar 17 16:07:03 2012 +0100
@@ -9,7 +9,7 @@
 sig
   val define: (((binding * typ) * mixfix) * (binding * term) ->
       term list * term list -> local_theory -> (term * thm) * local_theory) ->
-    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+    bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
       (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
@@ -48,7 +48,7 @@
 
 (* define *)
 
-fun define foundation ((b, mx), ((b_def, atts), rhs)) lthy =
+fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
     val thy_ctxt = Proof_Context.init_global thy;
@@ -88,7 +88,8 @@
 
     (*note*)
     val ([(res_name, [res])], lthy4) = lthy3
-      |> Local_Theory.notes_kind "" [((b_def, atts), [([def], [])])];
+      |> Local_Theory.notes_kind ""
+        [((if internal then Binding.empty else b_def, atts), [([def], [])])];
   in ((lhs, (res_name, res)), lthy4) end;
 
 
diff -r 196f2d9406c4 -r eeea81b86b70 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Mar 17 15:33:08 2012 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Mar 17 16:07:03 2012 +0100
@@ -32,6 +32,8 @@
   val global_morphism: local_theory -> morphism
   val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
+  val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+    (term * (string * thm)) * local_theory
   val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   val notes: (Attrib.binding * (thm list * Attrib.src list) list) list ->
     local_theory -> (string * thm list) list * local_theory
@@ -63,7 +65,7 @@
 (* type lthy *)
 
 type operations =
- {define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+ {define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -195,7 +197,8 @@
 
 val pretty = operation #pretty;
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
-val define = apsnd checkpoint oo operation1 #define;
+val define = apsnd checkpoint oo operation2 #define false;
+val define_internal = apsnd checkpoint oo operation2 #define true;
 val notes_kind = apsnd checkpoint ooo operation2 #notes;
 val declaration = checkpoint ooo operation2 #declaration;
 
diff -r 196f2d9406c4 -r eeea81b86b70 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 17 15:33:08 2012 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 17 16:07:03 2012 +0100
@@ -214,7 +214,7 @@
           in (b, mx) end);
     val name = Thm.def_binding_optional b raw_name;
     val ((lhs, (_, raw_th)), lthy2) = lthy
-      |> Local_Theory.define (var, ((Binding.suffix_name "_raw" name, []), rhs));
+      |> Local_Theory.define_internal (var, ((Binding.suffix_name "_raw" name, []), rhs));
 
     val th = prove lthy2 raw_th;
     val lthy3 = lthy2 |> Spec_Rules.add Spec_Rules.Equational ([lhs], [th]);