1.1 --- a/src/Pure/Isar/specification.ML	Thu Nov 09 21:44:32 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Nov 09 21:44:33 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 -> local_theory
     1.8 +    local_theory -> (term * term) list * local_theory
     1.9    val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
    1.10 -    local_theory -> local_theory
    1.11 +    local_theory -> (term * term) list * 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 @@ -132,7 +132,7 @@
    1.16            |> LocalTheory.def ((x, mx), ((name, []), rhs));
    1.17          val ((b, [th']), lthy3) = lthy2
    1.18            |> LocalTheory.note ((name, atts), [prove lthy2 th]);
    1.19 -      in (((x, T), (lhs, (b, th'))), LocalTheory.reinit lthy3) end;
    1.20 +      in (((x, T), (lhs, (b, th'))), LocalTheory.restore lthy3) end;
    1.21  
    1.22      val ((cs, defs), lthy') = lthy |> fold_map define args |>> split_list;
    1.23      val def_frees = member (op =) (fold (Term.add_frees o fst) defs []);
    1.24 @@ -153,21 +153,19 @@
    1.25            prep (the_list raw_var) [(("", []), [raw_prop])]
    1.26              (lthy1 |> ProofContext.expand_abbrevs false);
    1.27          val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy1 prop));
    1.28 -        val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
    1.29 -          if x = x' then mx
    1.30 -          else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote x'));
    1.31 -      in
    1.32 -        lthy1
    1.33 -        |> LocalTheory.abbrevs mode [((x, mx), rhs)]
    1.34 -        |> pair (x, T)
    1.35 -      end;
    1.36 +        val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
    1.37 +          if x = y then mx
    1.38 +          else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
    1.39 +        val ([abbr], lthy2) = lthy1
    1.40 +          |> LocalTheory.abbrevs mode [((x, mx), rhs)];
    1.41 +      in (((x, T), abbr), LocalTheory.restore lthy2) end;
    1.42  
    1.43 -    val (cs, lthy1) = lthy
    1.44 +    val (abbrs, lthy1) = lthy
    1.45        |> ProofContext.set_syntax_mode mode
    1.46        |> fold_map abbrev args
    1.47        ||> ProofContext.restore_syntax_mode lthy;
    1.48 -    val _ = print_consts lthy1 (K false) cs;
    1.49 -  in lthy1 end;
    1.50 +    val _ = print_consts lthy1 (K false) (map fst abbrs);
    1.51 +  in (map snd abbrs, lthy1) end;
    1.52  
    1.53  val abbreviation = gen_abbrevs read_specification;
    1.54  val abbreviation_i = gen_abbrevs cert_specification;
    1.55 @@ -261,7 +259,7 @@
    1.56      val (loc, ctxt, lthy) =
    1.57        (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
    1.58          (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)
    1.59 -          (SOME loc, ProofContext.init thy, LocalTheory.reinit lthy0)
    1.60 +          (SOME loc, ProofContext.init thy, LocalTheory.restore lthy0)
    1.61        | _ => (NONE, lthy0, lthy0));
    1.62  
    1.63      val elems = raw_elems |> (map o Locale.map_elem)