# HG changeset patch
# User wenzelm
# Date 1268949584 -3600
# Node ID 51c6ac100bd9e545d0445c46151a265d62e721d8
# Parent  0c71e0d72d7a6ac35136c1f2110a537a3f8da6dd
typedecl: no sort constraints;

diff -r 0c71e0d72d7a -r 51c6ac100bd9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Mar 18 22:56:32 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 18 22:59:44 2010 +0100
@@ -105,7 +105,7 @@
 val _ =
   OuterSyntax.local_theory "typedecl" "type declaration" K.thy_decl
     (P.type_args -- P.binding -- P.opt_mixfix
-      >> (fn ((args, a), mx) => Typedecl.typedecl (a, args, mx) #> snd));
+      >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
 
 val _ =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl