removing previously used function locally_monomorphic in the code generator
authorbulwahn
Wed Sep 07 13:51:39 2011 +0200 (2011-09-07)
changeset 447967f1f164696a4
parent 44795 238c6c7da908
child 44797 e0da66339e47
removing previously used function locally_monomorphic in the code generator
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:38 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:39 2011 +0200
     1.3 @@ -55,7 +55,6 @@
     1.4    val is_IAbs: iterm -> bool
     1.5    val eta_expand: int -> const * iterm list -> iterm
     1.6    val contains_dict_var: iterm -> bool
     1.7 -  val locally_monomorphic: iterm -> bool
     1.8    val add_constnames: iterm -> string list -> string list
     1.9    val add_tyconames: iterm -> string list -> string list
    1.10    val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
    1.11 @@ -262,12 +261,6 @@
    1.12        | cont_term (_ `|=> t) = cont_term t
    1.13        | cont_term (ICase (_, t)) = cont_term t;
    1.14    in cont_term t end;
    1.15 -  
    1.16 -fun locally_monomorphic (IConst _) = false
    1.17 -  | locally_monomorphic (IVar _) = true
    1.18 -  | locally_monomorphic (t `$ _) = locally_monomorphic t
    1.19 -  | locally_monomorphic (_ `|=> t) = locally_monomorphic t
    1.20 -  | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
    1.21  
    1.22  
    1.23  (** namings **)