# HG changeset patch
# User wenzelm
# Date 777303444 -7200
# Node ID a7f397a14b161f685659bfe3051a42144bfe2276
# Parent  c7d9018cc9e6fac97487b6641f8d4416ed751973
removed idT, varT, tidT, tvarT (now in lexicon.ML);
added syn_ext_const_names, syn_ext_trfuns;

diff -r c7d9018cc9e6 -r a7f397a14b16 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Fri Aug 19 15:37:05 1994 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Fri Aug 19 15:37:24 1994 +0200
@@ -18,10 +18,6 @@
   local open Ast in
     val logic: string
     val args: string
-    val idT: typ
-    val varT: typ
-    val tidT: typ
-    val tvarT: typ
     val applC: string
     val typ_to_nonterm: typ -> string
     datatype xsymb =
@@ -49,8 +45,13 @@
       (string * (ast list -> ast)) list * (string * (term list -> term)) list *
       (string * (term list -> term)) list * (string * (ast list -> ast)) list
       -> (ast * ast) list * (ast * ast) list -> syn_ext
+    val syn_ext_roots: string list -> string list -> syn_ext
+    val syn_ext_const_names: string list -> string list -> syn_ext
     val syn_ext_rules: string list -> (ast * ast) list * (ast * ast) list -> syn_ext
-    val syn_ext_roots: string list -> string list -> syn_ext
+    val syn_ext_trfuns: string list ->
+      (string * (ast list -> ast)) list * (string * (term list -> term)) list *
+      (string * (term list -> term)) list * (string * (ast list -> ast)) list
+      -> syn_ext
   end
 end;
 
@@ -79,14 +80,6 @@
 val funT = Type ("fun", []);
 
 
-(* terminals *)
-
-val idT = Type (id, []);
-val varT = Type (var, []);
-val tidT = Type (tid, []);
-val tvarT = Type (tvar, []);
-
-
 (* constants *)
 
 val applC = "_appl";
@@ -292,7 +285,7 @@
       Mfix ("_", to --> change_name from "_A", "", [0], 0);
 
     (* Make parentheses production for 'hidden' and 'automatic' nonterminal *)
-    fun parents T = 
+    fun parents T =
       if T = typeT then
         [Mfix ("'(_')", T --> T, "", [0], max_pri)]
       else
@@ -300,7 +293,7 @@
          Mfix ("'(_')", change_name T "_A" --> change_name T "_A", "", [0], max_pri)];
 
     fun mkappl T =
-      Mfix ("(1_/(1'(_')))", [funT, argsT] ---> change_name T "_A", applC, 
+      Mfix ("(1_/(1'(_')))", [funT, argsT] ---> change_name T "_A", applC,
             [max_pri, 0], max_pri);
 
     fun mkid T =
@@ -310,7 +303,7 @@
       Mfix ("_", varT --> change_name T "_A", "", [], max_pri);
 
     fun constrain T =
-      Mfix ("_::_", [T, typeT] ---> change_name T "_A", constrainC, 
+      Mfix ("_::_", [T, typeT] ---> change_name T "_A", constrainC,
             [4, 0], 3)
 
     fun unhide T =
@@ -332,7 +325,7 @@
   in
     SynExt {
       roots = new_roots,
-      xprods = (map (hide_xprod (all_roots \\ ["logic", "type"])) xprods) 
+      xprods = (map (hide_xprod (all_roots \\ ["logic", "type"])) xprods)
                @ xprods',    (* hide only productions that weren't created
                                 automatically *)
       consts = filter is_xid (consts union mfix_consts),
@@ -345,13 +338,17 @@
   end;
 
 
-(* syn_ext_rules, syn_ext_roots *)
+fun syn_ext_roots roots new_roots =
+  syn_ext roots new_roots [] [] ([], [], [], []) ([], []);
+
+fun syn_ext_const_names roots cs =
+  syn_ext roots [] [] cs ([], [], [], []) ([], []);
 
 fun syn_ext_rules roots rules =
   syn_ext roots [] [] [] ([], [], [], []) rules;
 
-fun syn_ext_roots all_roots new_roots =
-  syn_ext all_roots new_roots [] [] ([], [], [], []) ([], []);
+fun syn_ext_trfuns roots trfuns =
+  syn_ext roots [] [] [] trfuns ([], []);
 
 
 end;