tuned;
authorwenzelm
Fri Oct 31 15:21:32 1997 +0100 (1997-10-31)
changeset 4054b33e02b3478e
parent 4053 c88d0d5ae806
child 4055 69892b85f800
tuned;
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Oct 31 15:20:20 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Oct 31 15:21:32 1997 +0100
     1.3 @@ -9,7 +9,6 @@
     1.4  sig
     1.5    val typeT: typ
     1.6    val constrainC: string
     1.7 -  val mixfix_args: string -> int
     1.8  end;
     1.9  
    1.10  signature SYN_EXT =
    1.11 @@ -44,6 +43,7 @@
    1.12        print_rules: (Ast.ast * Ast.ast) list,
    1.13        print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.14        token_translation: (string * string * (string -> string * int)) list}
    1.15 +  val mfix_args: string -> int
    1.16    val mk_syn_ext: bool -> string list -> mfix list ->
    1.17      string list -> (string * (Ast.ast list -> Ast.ast)) list *
    1.18      (string * (term list -> term)) list *
    1.19 @@ -195,8 +195,8 @@
    1.20    val scan_mixfix = scan_symbs o SymbolFont.read_charnames o explode;
    1.21  end;
    1.22  
    1.23 -fun mixfix_args mx =
    1.24 -  foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, scan_mixfix mx);
    1.25 +fun mfix_args sy =
    1.26 +  foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, scan_mixfix sy);
    1.27  
    1.28  
    1.29  (* mfix_to_xprod *)
    1.30 @@ -249,11 +249,9 @@
    1.31      fun is_delim (Delim _) = true
    1.32        | is_delim _ = false;
    1.33  
    1.34 -    (*replace logical types on rhs by "logic"*)
    1.35 -    fun unify_logtypes copy_prod (a as (Argument (s, p))) =
    1.36 -          if s mem logtypes then Argument (logic, p)
    1.37 -          else a
    1.38 -      | unify_logtypes _ a = a;
    1.39 +    fun logify_types copy_prod (a as (Argument (s, p))) =
    1.40 +          if s mem logtypes then Argument (logic, p) else a
    1.41 +      | logify_types _ a = a;
    1.42  
    1.43  
    1.44      val raw_symbs = scan_mixfix sy handle ERROR => err "";
    1.45 @@ -268,7 +266,7 @@
    1.46         (if lhs mem logtypes then logic
    1.47          else if lhs = "prop" then sprop else lhs)
    1.48        else lhs;
    1.49 -    val symbs' = map (unify_logtypes copy_prod) symbs;
    1.50 +    val symbs' = map (logify_types copy_prod) symbs;
    1.51      val xprod = XProd (lhs', symbs', const, pri);
    1.52    in
    1.53      seq check_pri pris;