# HG changeset patch
# User wenzelm
# Date 856539784 -3600
# Node ID d73a46247a4a952f0baa7a36e04faf21ad8444a3
# Parent  585cd2311a98578c76f2dc5c695fbccbf01a06b3
declared the dummy type;

diff -r 585cd2311a98 -r d73a46247a4a src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Feb 21 16:35:49 1997 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 21 16:43:04 1997 +0100
@@ -156,7 +156,7 @@
 val pure_types =
   map (fn t => (t, 0, NoSyn))
     (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
-      "pttrn", "idt", "idts", "aprop", "asms", any, sprop]);
+      "pttrn", "idt", "idts", "aprop", "asms", any, sprop, "dummy"]);
 
 val pure_syntax =
  [("_lambda",   "[idts, 'a] => logic",            Mixfix ("(3%_./ _)", [], 0)),