remove dead code
authorhuffman
Mon, 12 Apr 2010 16:21:27 -0700
changeset 36119 ff605b8fdfdb
parent 36118 413d6d1f0f6e
child 36120 dd6e69cdcc1e
remove dead code
src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Apr 12 16:04:32 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Apr 12 16:21:27 2010 -0700
@@ -39,7 +39,6 @@
 
 (* ----- general testing and preprocessing of constructor list -------------- *)
 fun check_and_sort_domain
-    (definitional : bool)
     (dtnvs : (string * typ list) list)
     (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list)
     (thy : theory)
@@ -80,9 +79,6 @@
           | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
           | rm_sorts (TVar(s,_))  = TVar(s,[])
         and remove_sorts l = map rm_sorts l;
-        val indirect_ok =
-            [@{type_name "*"}, @{type_name cfun}, @{type_name ssum},
-             @{type_name sprod}, @{type_name u}];
         fun analyse indirect (TFree(v,s))  =
             (case AList.lookup (op =) tvars v of 
                NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
@@ -93,10 +89,7 @@
                                         " for type variable " ^ quote v))
           | analyse indirect (t as Type(s,typl)) =
             (case AList.lookup (op =) dtnvs s of
-               NONE =>
-                 if definitional orelse s mem indirect_ok
-                 then Type(s,map (analyse false) typl)
-                 else Type(s,map (analyse true) typl)
+               NONE => Type (s, map (analyse false) typl)
              | SOME typevars =>
                  if indirect 
                  then error ("Indirect recursion of type " ^ 
@@ -168,7 +161,7 @@
         map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
-        check_and_sort_domain true dtnvs' cons'' tmp_thy;
+        check_and_sort_domain dtnvs' cons'' tmp_thy;
     val dts : typ list = map (Type o fst) eqs';
 
     fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;