--- 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);