1.1 --- a/src/Pure/Isar/named_target.ML	Thu Aug 26 13:09:12 2010 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Thu Aug 26 15:48:08 2010 +0200
     1.3 @@ -118,7 +118,7 @@
     1.4        (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
     1.5    in
     1.6      lthy
     1.7 -    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
     1.8 +    |> Local_Theory.background_theory (PureThy.note_thmss kind global_facts' #> snd)
     1.9      |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
    1.10    end
    1.11  
    1.12 @@ -129,19 +129,21 @@
    1.13  
    1.14  (* abbrev *)
    1.15  
    1.16 -fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
    1.17 -  (Sign.add_abbrev Print_Mode.internal (b, t)) #->
    1.18 -    (fn (lhs, _) => locale_const_declaration ta prmode
    1.19 -      ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
    1.20 +fun locale_abbrev ta prmode ((b, mx), t) xs =
    1.21 +  Local_Theory.background_theory_result
    1.22 +    (Sign.add_abbrev Print_Mode.internal (b, t)) #->
    1.23 +      (fn (lhs, _) => locale_const_declaration ta prmode
    1.24 +        ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
    1.25  
    1.26  fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
    1.27      prmode (b, mx) (global_rhs, t') xs lthy =
    1.28 -  if is_locale
    1.29 -    then lthy
    1.30 -      |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
    1.31 -      |> is_class ? Class.abbrev target prmode ((b, mx), t')
    1.32 -    else lthy
    1.33 -      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
    1.34 +  if is_locale then
    1.35 +    lthy
    1.36 +    |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
    1.37 +    |> is_class ? Class.abbrev target prmode ((b, mx), t')
    1.38 +  else
    1.39 +    lthy
    1.40 +    |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
    1.41  
    1.42  
    1.43  (* pretty *)
    1.44 @@ -200,9 +202,10 @@
    1.45  
    1.46  fun init target thy = init_target (named_target thy target) thy;
    1.47  
    1.48 -fun reinit lthy = case peek lthy
    1.49 - of SOME {target, ...} => init target o Local_Theory.exit_global
    1.50 -  | NONE => error "Not in a named target";
    1.51 +fun reinit lthy =
    1.52 +  (case peek lthy of
    1.53 +    SOME {target, ...} => init target o Local_Theory.exit_global
    1.54 +  | NONE => error "Not in a named target");
    1.55  
    1.56  val theory_init = init_target global_target;
    1.57