diff -r b254814a094c -r 5895c525739d src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Wed Dec 01 15:02:39 2010 +0100
+++ b/src/CCL/CCL.thy	Wed Dec 01 15:03:44 2010 +0100
@@ -233,7 +233,7 @@
          | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
          | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
            val T = Sign.the_const_type thy (Sign.intern_const thy sy);
-           val arity = length (fst (strip_type T))
+           val arity = length (binder_types T)
        in sy ^ (arg_str arity name "") end
 
   fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")