src/Pure/Isar/generic_target.ML

 
 (* abbrev *)
 
 fun background_abbrev (b, global_rhs) params =
   Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
-  #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, params), Logic.unvarify_global rhs))
+  #>> pairself (fn t => Term.list_comb (Logic.unvarify_global t, params))
 
 fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
   let
     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);