removed mixfix_content;
authorwenzelm
Fri Sep 29 22:47:04 2006 +0200 (2006-09-29)
changeset 2078696077403f619
parent 20785 d60f81c56fd4
child 20787 406d990006af
removed mixfix_content;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Sep 29 22:47:03 2006 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Sep 29 22:47:04 2006 +0200
     1.3 @@ -32,7 +32,6 @@
     1.4    val const_mixfix: string -> mixfix -> string * mixfix
     1.5    val unlocalize_mixfix: mixfix -> mixfix
     1.6    val mixfix_args: mixfix -> int
     1.7 -  val mixfix_content: mixfix -> string list list
     1.8  end;
     1.9  
    1.10  signature MIXFIX =
    1.11 @@ -232,19 +231,4 @@
    1.12        mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
    1.13    end;
    1.14  
    1.15 -fun mixfix_content mx =
    1.16 -  let
    1.17 -    fun delims sy = SynExt.mfix_delims sy;
    1.18 -    fun op_delims sy = let val ds = delims sy in ["op" :: ds, ds] end;
    1.19 -  in
    1.20 -    case mx of
    1.21 -      Mixfix (sy, _, _) => [delims sy]
    1.22 -    | Delimfix sy => [delims sy]
    1.23 -    | InfixName (sy, _) => op_delims sy
    1.24 -    | InfixlName (sy, _) => op_delims sy
    1.25 -    | InfixrName (sy, _) => op_delims sy
    1.26 -    | Binder (sy, _, _) => [delims sy @ ["."]]
    1.27 -    | _ => []
    1.28 -  end;
    1.29 -
    1.30  end;