# HG changeset patch
# User wenzelm
# Date 787397094 -3600
# Node ID 567f1fe7ea390f22464ba73a407343e1d4cea529
# Parent  4ab9176b45b71ef0ba205d7dec10534118acf5a0
removed "logic1";
improved typ_to_nonterm;

diff -r 4ab9176b45b7 -r 567f1fe7ea39 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Tue Dec 13 11:51:12 1994 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Dec 14 10:24:54 1994 +0100
@@ -18,6 +18,8 @@
   local open Ast in
     val logic: string
     val args: string
+    val any: string
+    val sprop: string
     val applC: string
     val typ_to_nonterm: typ -> string
     datatype xsymb =
@@ -42,7 +44,7 @@
         print_rules: (ast * ast) list,
         print_ast_translation: (string * (ast list -> ast)) list}
     val mk_syn_ext: bool -> string list -> mfix list ->
-      string list -> (string * (ast list -> ast)) list * 
+      string list -> (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
@@ -75,8 +77,6 @@
 val logic = "logic";
 val logicT = Type (logic, []);
 
-val logic1 = "logic1";
-
 val args = "args";
 val argsT = Type (args, []);
 
@@ -88,6 +88,7 @@
 val any = "any";
 val anyT = Type (any, []);
 
+
 (* constants *)
 
 val applC = "_appl";
@@ -151,11 +152,11 @@
 (* typ_to_nonterm *)
 
 (*get nonterminal for rhs*)
-fun typ_to_nonterm (Type (c, _)) = if c="fun" then logic else c
+fun typ_to_nonterm (Type (c, _)) = c
   | typ_to_nonterm _ = any;
 
 (*get nonterminal for lhs*)
-fun typ_to_nonterm1 (ty as Type (c, _)) = typ_to_nonterm ty
+fun typ_to_nonterm1 (Type (c, _)) = c
   | typ_to_nonterm1 _ = logic;
 
 
@@ -164,7 +165,7 @@
 fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
   let
     fun err msg =
-      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " 
+      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for "
                 ^ quote const);
         error msg);