# HG changeset patch
# User wenzelm
# Date 895054853 -7200
# Node ID 9c4ff93762a05d7bca4af1dce54ceb881a351b7e
# Parent  9397b1446cdb3d084a6ca88efdf0f6491e53e655
pure_nonterms;

diff -r 9397b1446cdb -r 9c4ff93762a0 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed May 13 12:20:28 1998 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed May 13 12:20:53 1998 +0200
@@ -26,7 +26,7 @@
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
   val mixfix_args: mixfix -> int
-  val pure_types: (string * int * mixfix) list
+  val pure_nonterms: string list
   val pure_syntax: (string * string * mixfix) list
   val pure_appl_syntax: (string * string * mixfix) list
   val pure_applC_syntax: (string * string * mixfix) list
@@ -165,10 +165,9 @@
 
 (** Pure syntax **)
 
-val pure_types =
-  map (fn t => (t, 0, NoSyn))
-    (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
-      "pttrn", "pttrns", "idt", "idts", "aprop", "asms", any, sprop, "dummy"]);
+val pure_nonterms =
+  (terminals @ [logic, "type", "types", "sort", "classes", args, cargs,
+    "pttrn", "pttrns", "idt", "idts", "aprop", "asms", any, sprop]);
 
 val pure_syntax =
  [("_lambda",      "[pttrns, 'a] => logic",         Mixfix ("(3%_./ _)", [0, 3], 3)),