pure_nonterms;
authorwenzelm
Wed, 13 May 1998 12:20:53 +0200
changeset 4920 9c4ff93762a0
parent 4919 9397b1446cdb
child 4921 74bc10921f7d
pure_nonterms;
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)),