# HG changeset patch
# User bulwahn
# Date 1315396299 -7200
# Node ID 7f1f164696a4d981c7a48e577a4c3caf5e2ce631
# Parent  238c6c7da908d57e0f0372bed91c2b7800f2ca73
removing previously used function locally_monomorphic in the code generator

diff -r 238c6c7da908 -r 7f1f164696a4 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:38 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:39 2011 +0200
@@ -55,7 +55,6 @@
   val is_IAbs: iterm -> bool
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dict_var: iterm -> bool
-  val locally_monomorphic: iterm -> bool
   val add_constnames: iterm -> string list -> string list
   val add_tyconames: iterm -> string list -> string list
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
@@ -262,12 +261,6 @@
       | cont_term (_ `|=> t) = cont_term t
       | cont_term (ICase (_, t)) = cont_term t;
   in cont_term t end;
-  
-fun locally_monomorphic (IConst _) = false
-  | locally_monomorphic (IVar _) = true
-  | locally_monomorphic (t `$ _) = locally_monomorphic t
-  | locally_monomorphic (_ `|=> t) = locally_monomorphic t
-  | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
 
 
 (** namings **)