--- 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"