src/Pure/Syntax/syn_ext.ML

 
 signature SYN_EXT0 =
 sig
   val typeT: typ
   val constrainC: string
-  val mixfix_args: string -> int
 end;
 
 signature SYN_EXT =
 sig
   include SYN_EXT0

       parse_translation: (string * (term list -> term)) list,
       print_translation: (string * (typ -> term list -> term)) list,
       print_rules: (Ast.ast * Ast.ast) list,
       print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
       token_translation: (string * string * (string -> string * int)) list}
+  val mfix_args: string -> int
   val mk_syn_ext: bool -> string list -> mfix list ->
     string list -> (string * (Ast.ast list -> Ast.ast)) list *
     (string * (term list -> term)) list *
     (string * (typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
     -> (string * string * (string -> string * int)) list

   val scan_symbs = mapfilter I o #1 o repeat scan_symb;
 in
   val scan_mixfix = scan_symbs o SymbolFont.read_charnames o explode;
 end;
 
-fun mixfix_args mx =
-  foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, scan_mixfix mx);
+fun mfix_args sy =
+  foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, scan_mixfix sy);
 
 
 (* mfix_to_xprod *)
 
 fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =

       | rem_pri sym = sym;
 
     fun is_delim (Delim _) = true
       | is_delim _ = false;
 
-    (*replace logical types on rhs by "logic"*)
-    fun unify_logtypes copy_prod (a as (Argument (s, p))) =
-          if s mem logtypes then Argument (logic, p)
-          else a
-      | unify_logtypes _ a = a;
+    fun logify_types copy_prod (a as (Argument (s, p))) =
+          if s mem logtypes then Argument (logic, p) else a
+      | logify_types _ a = a;
 
 
     val raw_symbs = scan_mixfix sy handle ERROR => err "";
     val (symbs, lhs) = add_args raw_symbs typ pris;
     val copy_prod =

     val lhs' =
       if convert andalso not copy_prod then
        (if lhs mem logtypes then logic
         else if lhs = "prop" then sprop else lhs)
       else lhs;
-    val symbs' = map (unify_logtypes copy_prod) symbs;
+    val symbs' = map (logify_types copy_prod) symbs;
     val xprod = XProd (lhs', symbs', const, pri);
   in
     seq check_pri pris;
     check_pri pri;
     check_blocks symbs';