# HG changeset patch
# User haftmann
# Date 1433177960 -7200
# Node ID fcbd7f0c52c3d26abf381aea7c035f73f30e7252
# Parent  69394731c4194de6a7dfc1abc0db40cf83080d78
clearly separated target primitives (target_foo) from self-contained target operations (foo)

diff -r 69394731c419 -r fcbd7f0c52c3 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/class.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -580,7 +580,7 @@
     SOME c =>
       if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
       else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs)
-  | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
+  | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
   let
@@ -645,8 +645,8 @@
     |> synchronize_inst_syntax
     |> Local_Theory.init (Sign.naming_of thy)
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes Generic_Target.theory_notes,
-        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+        notes = Generic_Target.notes Generic_Target.theory_target_notes,
+        abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         subscription = Generic_Target.theory_registration,
         pretty = pretty,
diff -r 69394731c419 -r fcbd7f0c52c3 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -31,29 +31,33 @@
       term list * term list -> local_theory -> local_theory) ->
     Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
 
-  (*theory operations*)
-  val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
-    term list * term list -> local_theory -> (term * thm) * local_theory
-  val theory_notes: string ->
+  (*theory target primitives*)
+  val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+     term list * term list -> local_theory -> (term * thm) * local_theory
+  val theory_target_notes: string ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
+  val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
+    local_theory -> local_theory
+
+  (*theory target operations*)
   val theory_declaration: declaration -> local_theory -> local_theory
-  val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
-    local_theory -> local_theory
   val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
 
-  (*locale operations*)
-  val locale_notes: string -> string ->
+  (*locale target primitives*)
+  val locale_target_notes: string -> string ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     local_theory -> local_theory
   val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
+  val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
+    (binding * mixfix) * term -> local_theory -> local_theory
+
+  (*locale operations*)
   val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration ->
     local_theory -> local_theory
-  val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
-    (binding * mixfix) * term -> local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
   val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
@@ -259,7 +263,7 @@
 
 in
 
-fun notes notes' kind facts lthy =
+fun notes target_notes kind facts lthy =
   let
     val facts' = facts
       |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi
@@ -269,7 +273,7 @@
     val global_facts = Global_Theory.map_facts #2 facts';
   in
     lthy
-    |> notes' kind global_facts (Attrib.partial_evaluation lthy local_facts)
+    |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts)
     |> Attrib.local_notes kind local_facts
   end;
 
@@ -278,7 +282,7 @@
 
 (* abbrev *)
 
-fun abbrev abbrev' prmode ((b, mx), rhs) lthy =
+fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
 
@@ -293,28 +297,25 @@
     val type_params = map (Logic.mk_type o TFree) extra_tfrees;
   in
     lthy
-    |> abbrev' prmode (b, mx') global_rhs (type_params, term_params)
+    |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params)
     |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd
     |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs)
   end;
 
 
 
-(** theory operations **)
+(** theory target primitives **)
 
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def));
 
-fun theory_notes kind global_facts local_facts =
+fun theory_target_notes kind global_facts local_facts =
   Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd)
   #> standard_notes (op <>) kind local_facts;
 
-fun theory_declaration decl =
-  background_declaration decl #> standard_declaration (K true) decl;
-
-fun theory_abbrev prmode (b, mx) global_rhs params =
+fun theory_target_abbrev prmode (b, mx) global_rhs params =
   Local_Theory.background_theory_result
     (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
       (fn (lhs, _) =>  (* FIXME type_params!? *)
@@ -322,14 +323,20 @@
   #-> (fn lhs => standard_const (op <>) prmode
           ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params)));
 
+
+(** theory operations **)
+
+fun theory_declaration decl =
+  background_declaration decl #> standard_declaration (K true) decl;
+
 val theory_registration =
   Local_Theory.raw_theory o Context.theory_map ooo Locale.add_registration;
 
 
 
-(** locale operations **)
+(** locale target primitives **)
 
-fun locale_notes locale kind global_facts local_facts =
+fun locale_target_notes locale kind global_facts local_facts =
   Local_Theory.background_theory
     (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #>
   (fn lthy => lthy |>
@@ -342,14 +349,17 @@
     Locale.add_declaration locale syntax
       (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
 
+fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
+  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
+
+
+(** locale operations **)
+
 fun locale_declaration locale {syntax, pervasive} decl =
   pervasive ? background_declaration decl
   #> locale_target_declaration locale syntax decl
   #> standard_declaration (fn (_, other) => other <> 0) decl;
 
-fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
-  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
-
 fun locale_const locale prmode ((b, mx), rhs) =
   locale_target_const locale (K true) prmode ((b, mx), rhs)
   #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
diff -r 69394731c419 -r fcbd7f0c52c3 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/named_target.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -75,15 +75,15 @@
   #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params
     #> pair (lhs, def));
 
-fun foundation ("", _) = Generic_Target.theory_foundation
+fun foundation ("", _) = Generic_Target.theory_target_foundation
   | foundation (locale, false) = locale_foundation locale
   | foundation (class, true) = class_foundation class;
 
 
 (* notes *)
 
-fun notes ("", _) = Generic_Target.theory_notes
-  | notes (locale, _) = Generic_Target.locale_notes locale;
+fun notes ("", _) = Generic_Target.theory_target_notes
+  | notes (locale, _) = Generic_Target.locale_target_notes locale;
 
 
 (* abbrev *)
@@ -96,7 +96,7 @@
   Generic_Target.background_abbrev (b, global_rhs) (snd params)
   #-> (fn (lhs, rhs) => Class.abbrev class prmode ((b, mx), lhs) rhs params);
 
-fun abbrev ("", _) = Generic_Target.theory_abbrev
+fun abbrev ("", _) = Generic_Target.theory_target_abbrev
   | abbrev (locale, false) = locale_abbrev locale
   | abbrev (class, true) = class_abbrev class;
 
diff -r 69394731c419 -r fcbd7f0c52c3 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -161,7 +161,7 @@
       if mx <> NoSyn
       then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
       else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
-  | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
+  | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
   let
@@ -201,8 +201,8 @@
     |> synchronize_syntax
     |> Local_Theory.init (Sign.naming_of thy)
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes Generic_Target.theory_notes,
-        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+        notes = Generic_Target.notes Generic_Target.theory_target_notes,
+        abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         subscription = Generic_Target.theory_registration,
         pretty = pretty,