removing previously used function locally_monomorphic in the code generator
authorbulwahn
Wed, 07 Sep 2011 13:51:39 +0200
changeset 44796 7f1f164696a4
parent 44795 238c6c7da908
child 44797 e0da66339e47
removing previously used function locally_monomorphic in the code generator
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 **)