Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned;
authorwenzelm
Tue, 13 Dec 2011 20:10:36 +0100
changeset 45837 086ff24a9aa3
parent 45836 8bed07ec172b
child 45838 653c84d5c6c9
tuned;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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"
isabelle