--- a/src/Pure/Isar/generic_target.ML Thu May 22 17:53:01 2014 +0200
+++ b/src/Pure/Isar/generic_target.ML Thu May 22 17:53:01 2014 +0200
@@ -20,7 +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 background_abbrev: binding * term -> term list -> 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
@@ -198,8 +198,9 @@
(* abbrev *)
-fun background_abbrev (b, t) =
+fun background_abbrev (b, t) xs =
Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t))
+ #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, xs), rhs))
fun abbrev target_abbrev prmode ((b, mx), t) lthy =
let