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 **)