modernized old-style type abbreviations;

--- a/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 19:58:04 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 16 20:17:38 2010 +0200
@@ -13,6 +13,7 @@
   val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val add_tyabbrs: (binding * string list * string * mixfix) list -> local_theory -> local_theory
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: (Attrib.binding * string) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
@@ -149,6 +150,11 @@
 end;
 
 
+(* old-style type abbreviations *)
+
+val add_tyabbrs = fold (fn (a, args, rhs, mx) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs);
+
+
 (* oracles *)
 
 fun oracle (name, pos) (body_txt, body_pos) =

--- a/src/Pure/Isar/isar_syn.ML	Fri Apr 16 19:58:04 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Apr 16 20:17:38 2010 +0200
@@ -113,10 +113,10 @@
       >> (fn (((args, a), mx), rhs) => Typedecl.abbrev_cmd (a, args, mx) rhs #> snd));
 
 val _ =
-  OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
+  OuterSyntax.local_theory "types" "declare type abbreviations" K.thy_decl
     (Scan.repeat1
       (P.type_args -- P.binding -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_mixfix')))
-      >> (Toplevel.theory o Sign.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
+      >> (IsarCmd.add_tyabbrs o map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
 
 val _ =
   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"