src/HOLCF/domain/extender.ML
changeset 4188 1025a27b08f9
parent 4122 f63c283cefaf
child 4709 d24168720303
--- a/src/HOLCF/domain/extender.ML	Fri Nov 07 17:51:26 1997 +0100
+++ b/src/HOLCF/domain/extender.ML	Fri Nov 07 18:02:15 1997 +0100
@@ -84,14 +84,14 @@
     val eqs' = check_and_sort_domain (dtnvs,cons'') sg'';
     val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
     val dts  = map (Type o fst) eqs';
-    fun strip ss = drop (find ("'", ss)+1, ss);
+    fun strip ss = drop (find_index_eq "'" ss +1, ss);
     fun typid (Type  (id,_)   ) = hd     (explode (Sign.base_name id))
       | typid (TFree (id,_)   ) = hd (strip (tl (explode (Sign.base_name id))))
       | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
     fun cons cons' = (map (fn (con,syn,args) =>
 	((Syntax.const_name con syn),
 	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
-					find (tp,dts) handle LIST "find" => ~1),
+					find_index_eq tp dts),
 					sel,vn))
 	     (args,(mk_var_names(map (typid o third) args)))
 	 )) cons') : cons list;