1.1 --- a/src/Pure/Isar/specification.ML	Sun Nov 26 18:07:27 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Sun Nov 26 18:07:29 2006 +0100
     1.3 @@ -31,9 +31,9 @@
     1.4      ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
     1.5      local_theory -> (term * (bstring * thm)) list * local_theory
     1.6    val abbreviation: Syntax.mode -> ((string * string option * mixfix) option * string) list ->
     1.7 -    local_theory -> (term * term) list * local_theory
     1.8 +    local_theory -> local_theory
     1.9    val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
    1.10 -    local_theory -> (term * term) list * local_theory
    1.11 +    local_theory -> local_theory
    1.12    val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    1.13    val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.14    val theorems: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
    1.15 @@ -157,16 +157,15 @@
    1.16          val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
    1.17            if x = y then mx
    1.18            else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
    1.19 -        val ([abbr], lthy2) = lthy1
    1.20 -          |> LocalTheory.abbrevs mode [((x, mx), rhs)];
    1.21 -      in (((x, T), abbr), LocalTheory.restore lthy2) end;
    1.22 +        val lthy2 = lthy1 |> LocalTheory.abbrevs mode [((x, mx), rhs)];
    1.23 +      in ((x, T), LocalTheory.restore lthy2) end;
    1.24  
    1.25 -    val (abbrs, lthy1) = lthy
    1.26 +    val (cs, lthy') = lthy
    1.27        |> ProofContext.set_syntax_mode mode
    1.28        |> fold_map abbrev args
    1.29        ||> ProofContext.restore_syntax_mode lthy;
    1.30 -    val _ = print_consts lthy1 (K false) (map fst abbrs);
    1.31 -  in (map snd abbrs, lthy1) end;
    1.32 +    val _ = print_consts lthy' (K false) cs;
    1.33 +  in lthy' end;
    1.34  
    1.35  val abbreviation = gen_abbrevs read_specification;
    1.36  val abbreviation_i = gen_abbrevs cert_specification;
    1.37 @@ -269,8 +268,7 @@
    1.38      val attrib = prep_att thy;
    1.39      val atts = map attrib raw_atts;
    1.40  
    1.41 -    val elems = raw_elems |> (map o Locale.map_elem)
    1.42 -      (Element.map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib});
    1.43 +    val elems = raw_elems |> map (Locale.map_elem (Element.map_ctxt_attrib attrib));
    1.44      val ((prems, stmt, facts), goal_ctxt) =
    1.45        prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
    1.46