1.1 --- a/src/Pure/Isar/generic_target.ML	Wed May 28 19:17:32 2014 +0200
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Wed May 28 19:18:18 2014 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4  
     1.5  fun background_abbrev (b, global_rhs) params =
     1.6    Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
     1.7 -  #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, params), rhs))
     1.8 +  #>> (fn (lhs, rhs) => (Term.list_comb (Logic.unvarify_global lhs, params), Logic.unvarify_global rhs))
     1.9  
    1.10  fun abbrev target_abbrev prmode ((b, mx), rhs) lthy =
    1.11    let