--- a/src/HOLCF/Tools/Domain/domain_extender.ML Tue Nov 24 17:28:44 2009 +0100
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML Wed Nov 25 09:13:46 2009 +0100
@@ -153,7 +153,7 @@
val thy' = thy'' |> Domain_Syntax.add_syntax false comp_dnam eqs';
val dts = map (Type o fst) eqs';
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
+ fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
fun typid (Type (id,_)) =
let val c = hd (Symbol.explode (Long_Name.base_name id))
in if Symbol.is_letter c then c else "t" end
@@ -228,7 +228,7 @@
val thy' = thy'' |> Domain_Syntax.add_syntax true comp_dnam eqs';
val dts = map (Type o fst) eqs';
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = (uncurry drop) (find_index (fn s => s = "'") ss + 1, ss);
+ fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
fun typid (Type (id,_)) =
let val c = hd (Symbol.explode (Long_Name.base_name id))
in if Symbol.is_letter c then c else "t" end