# HG changeset patch
# User haftmann
# Date 1400770789 -7200
# Node ID 474403e50e052fc8a4f30d6057266b9c070ac81b
# Parent  b3571d1a3e45e0df4847a003bb541c72943bce33
common background_abbrev operation

diff -r b3571d1a3e45 -r 474403e50e05 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu May 22 16:59:49 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu May 22 16:59:49 2014 +0200
@@ -20,6 +20,7 @@
     (Attrib.binding * (thm list * Args.src list) list) list ->
     (Attrib.binding * (thm list * Args.src list) list) list ->
     local_theory -> local_theory
+  val background_abbrev: binding * term -> local_theory -> (term * term) * local_theory
   val abbrev: (string * bool -> binding * mixfix -> term * term ->
       term list -> local_theory -> local_theory) ->
     string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory
@@ -195,6 +196,9 @@
 
 (* abbrev *)
 
+fun background_abbrev (b, t) =
+  Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t))
+
 fun abbrev target_abbrev prmode ((b, mx), t) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
diff -r b3571d1a3e45 -r 474403e50e05 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu May 22 16:59:49 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu May 22 16:59:49 2014 +0200
@@ -122,12 +122,12 @@
 (* abbrev *)
 
 fun locale_abbrev target prmode (b, mx) (t, _) xs =
-  Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t))
+  Generic_Target.background_abbrev (b, t)
   #-> (fn (lhs, _) =>
         locale_const target prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
 fun class_abbrev target prmode (b, mx) (t, t') xs =
-  Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t))
+  Generic_Target.background_abbrev (b, t)
   #-> (fn (lhs, _) =>
         class_const target prmode (b, Term.list_comb (Logic.unvarify_global lhs, xs)))
   #> Class.abbrev target prmode ((b, mx), t');