# HG changeset patch
# User wenzelm
# Date 1137702145 -3600
# Node ID dd1ebba121511d8c097094eecc4fe98b5af9e4aa
# Parent  dca3ae4f6dd63dfe249860f211e9c747e1e50851
added basic syntax;
removed pure syntax;

diff -r dca3ae4f6dd6 -r dd1ebba12151 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Jan 19 21:22:24 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Jan 19 21:22:25 2006 +0100
@@ -60,7 +60,10 @@
     string * bool -> (string * typ * mixfix) list -> syntax -> syntax
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
   val merge_syntaxes: syntax -> syntax -> syntax
-  val pure_syn: syntax
+  val basic_syn: syntax
+  val basic_nonterms: string list
+  val appl_syntax: (string * string * mixfix) list
+  val applC_syntax: (string * string * mixfix) list
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
@@ -292,13 +295,28 @@
   end;
 
 
-(* pure_syn *)
+(* basic syntax *)
 
-val pure_syn =
+val basic_syn =
   empty_syntax
   |> extend_syntax default_mode TypeExt.type_ext
   |> extend_syntax default_mode SynExt.pure_ext;
 
+val basic_nonterms =
+  (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
+    SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
+    "asms", SynExt.any, SynExt.sprop, "num_const", "index", "struct"]);
+
+val appl_syntax =
+ [("_appl", "[('b => 'a), args] => logic", Mixfix.Mixfix ("(1_/(1'(_')))", [1000, 0], 1000)),
+  ("_appl", "[('b => 'a), args] => aprop", Mixfix.Mixfix ("(1_/(1'(_')))", [1000, 0], 1000))];
+
+val applC_syntax =
+ [("",       "'a => cargs",                  Mixfix.Delimfix "_"),
+  ("_cargs", "['a, cargs] => cargs",         Mixfix.Mixfix ("_/ _", [1000, 1000], 1000)),
+  ("_applC", "[('b => 'a), cargs] => logic", Mixfix.Mixfix ("(1_/ _)", [1000, 1000], 999)),
+  ("_applC", "[('b => 'a), cargs] => aprop", Mixfix.Mixfix ("(1_/ _)", [1000, 1000], 999))];
+
 
 
 (** print syntax **)