# HG changeset patch # User huffman # Date 1271114487 25200 # Node ID ff605b8fdfdb2073895461c4aced2392307571f1 # Parent 413d6d1f0f6e0770f13fb6c2b75bb452e87b3bce remove dead code diff -r 413d6d1f0f6e -r ff605b8fdfdb 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;