removed separate logtypes field of syntax;

--- a/src/Pure/Syntax/mixfix.ML	Wed Jun 09 18:54:07 2004 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Jun 09 18:54:26 2004 +0200
@@ -42,10 +42,8 @@
 signature MIXFIX =
 sig
   include MIXFIX1
-  val syn_ext_types: string list -> (string * int * mixfix) list
-    -> SynExt.syn_ext
-  val syn_ext_consts: string list -> (string * typ * mixfix) list
-    -> SynExt.syn_ext
+  val syn_ext_types: (string * int * mixfix) list -> SynExt.syn_ext
+  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
 end;
 
 
@@ -133,7 +131,7 @@
 
 (* syn_ext_types *)
 
-fun syn_ext_types logtypes type_decls =
+fun syn_ext_types type_decls =
   let
     fun name_of (t, _, mx) = type_name t mx;
 
@@ -151,17 +149,17 @@
         | (sy, 2, Infix p) => Some (mk_infix sy t (p + 1) (p + 1) p)
         | (sy, 2, Infixl p) => Some (mk_infix sy t p (p + 1) p)
         | (sy, 2, Infixr p) => Some (mk_infix sy t (p + 1) p p)
-        | _ => error ("Bad mixfix declaration for type " ^ quote t))
+        | _ => error ("Bad mixfix declaration for type: " ^ quote t))
       end;
 
     val mfix = mapfilter mfix_of type_decls;
     val xconsts = map name_of type_decls;
-  in SynExt.syn_ext logtypes mfix xconsts ([], [], [], []) [] ([], []) end;
+  in SynExt.syn_ext mfix xconsts ([], [], [], []) [] ([], []) end;
 
 
 (* syn_ext_consts *)
 
-fun syn_ext_consts logtypes const_decls =
+fun syn_ext_consts is_logtype const_decls =
   let
     fun name_of (c, _, mx) = const_name c mx;
 
@@ -171,7 +169,7 @@
 
     fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
           [Type ("idts", []), ty2] ---> ty3
-      | binder_typ c _ = error ("Bad type of binder " ^ quote c);
+      | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
 
     fun mfix_of decl =
       let val c = name_of decl in
@@ -198,7 +196,10 @@
     val binder_trs = map SynTrans.mk_binder_tr binders;
     val binder_trs' =
       map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders;
-  in SynExt.syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) end;
+  in
+    SynExt.syn_ext' true is_logtype
+      mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
+  end;
 
 
 

--- a/src/Pure/Syntax/syn_ext.ML	Wed Jun 09 18:54:07 2004 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Jun 09 18:54:26 2004 +0200
@@ -34,7 +34,6 @@
   datatype mfix = Mfix of string * typ * string * int list * int
   datatype syn_ext =
     SynExt of {
-      logtypes: string list,
       xprods: xprod list,
       consts: string list,
       prmodes: string list,
@@ -47,27 +46,25 @@
       token_translation: (string * string * (string -> string * real)) list}
   val mfix_args: string -> int
   val escape_mfix: string -> string
-  val mk_syn_ext: bool -> string list -> mfix list ->
+  val syn_ext': bool -> (string -> bool) -> mfix list ->
     string list -> (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
     (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
     -> (string * string * (string -> string * real)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
-  val syn_ext: string list -> mfix list -> string list ->
+  val syn_ext: mfix list -> string list ->
     (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
     (string * (bool -> typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
     -> (string * string * (string -> string * real)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
-  val syn_ext_logtypes: string list -> syn_ext
-  val syn_ext_const_names: string list -> string list -> syn_ext
-  val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
-  val syn_ext_trfuns: string list ->
+  val syn_ext_const_names: string list -> syn_ext
+  val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
+  val syn_ext_trfuns:
     (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
     (string * (bool -> typ -> term list -> term)) list *
     (string * (Ast.ast list -> Ast.ast)) list -> syn_ext
-  val syn_ext_tokentrfuns: string list
-    -> (string * string * (string -> string * real)) list -> syn_ext
+  val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
   val pure_ext: syn_ext
 end;
 
@@ -224,7 +221,7 @@
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod convert logtypes (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
   let
     fun check_pri p =
       if p >= 0 andalso p <= max_pri then ()
@@ -260,7 +257,7 @@
       | rem_pri sym = sym;
 
     fun logify_types copy_prod (a as (Argument (s, p))) =
-          if s mem logtypes then Argument (logic, p) else a
+          if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
       | logify_types _ a = a;
 
 
@@ -292,8 +289,7 @@
         andalso not (exists is_delim symbs);
     val lhs' =
       if convert andalso not copy_prod then
-       (if lhs mem logtypes then logic
-        else if lhs = "prop" then sprop else lhs)
+       (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
       else lhs;
     val symbs' = map (logify_types copy_prod) symbs;
     val xprod = XProd (lhs', symbs', const', pri);
@@ -315,7 +311,6 @@
 
 datatype syn_ext =
   SynExt of {
-    logtypes: string list,
     xprods: xprod list,
     consts: string list,
     prmodes: string list,
@@ -330,18 +325,16 @@
 
 (* syn_ext *)
 
-fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
+fun syn_ext' convert is_logtype mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
-    val logtypes' = logtypes \ "prop";
 
-    val (xprods, parse_rules') = map (mfix_to_xprod convert logtypes') mfixes
+    val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
       |> split_list |> apsnd (rev o flat);
     val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
   in
     SynExt {
-      logtypes = logtypes',
       xprods = xprods,
       consts = consts union_string mfix_consts,
       prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
@@ -355,27 +348,17 @@
   end;
 
 
-val syn_ext = mk_syn_ext true;
-
-fun syn_ext_logtypes logtypes =
-  syn_ext logtypes [] [] ([], [], [], []) [] ([], []);
-
-fun syn_ext_const_names logtypes cs =
-  syn_ext logtypes [] cs ([], [], [], []) [] ([], []);
+val syn_ext = syn_ext' true (K false);
 
-fun syn_ext_rules logtypes rules =
-  syn_ext logtypes [] [] ([], [], [], []) [] rules;
-
-fun syn_ext_trfuns logtypes trfuns =
-  syn_ext logtypes [] [] trfuns [] ([], []);
-
-fun syn_ext_tokentrfuns logtypes tokentrfuns =
-  syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []);
+fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) [] ([], []);
+fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) [] rules;
+fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns [] ([], []);
+fun syn_ext_tokentrfuns trfuns = syn_ext [] [] ([], [], [], []) trfuns ([], []);
 
 
 (* pure_ext *)
 
-val pure_ext = mk_syn_ext false []
+val pure_ext = syn_ext' false (K false)
   [Mfix ("_", spropT --> propT, "", [0], 0),
    Mfix ("_", logicT --> anyT, "", [0], 0),
    Mfix ("_", spropT --> anyT, "", [0], 0),

--- a/src/Pure/Syntax/type_ext.ML	Wed Jun 09 18:54:07 2004 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Wed Jun 09 18:54:26 2004 +0200
@@ -189,7 +189,7 @@
 
 local open Lexicon SynExt in
 
-val type_ext = mk_syn_ext false ["dummy"]
+val type_ext = syn_ext' false (K false)
   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    Mfix ("_",           idT --> typeT,                 "", [], max_pri),