# HG changeset patch
# User wenzelm
# Date 1323803436 -3600
# Node ID 086ff24a9aa3651d185d29e015ec3c3645006792
# Parent  8bed07ec172b31ad5bb4f72d5d489fa0c0ee0dae
tuned;

diff -r 8bed07ec172b -r 086ff24a9aa3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Dec 13 20:10:28 2011 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Dec 13 20:10:36 2011 +0100
@@ -113,13 +113,11 @@
     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
       >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
 
-val type_abbrev =
-  Parse.type_args -- Parse.binding --
-    (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'));
-
 val _ =
   Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl
-    (type_abbrev >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
+    (Parse.type_args -- Parse.binding --
+      (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
+      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
 
 val _ =
   Outer_Syntax.command "nonterminal"