src/CCL/CCL.ML

-(*  Title: 	CCL/ccl
+(*  Title:      CCL/ccl
     ID:         $Id$
-    Author: 	Martin Coen, Cambridge University Computer Laboratory
+    Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 For ccl.thy.
 *)
 

        let fun arg_str 0 a s = s
          | 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 sg = sign_of thy;
            val T = case Sign.const_type sg sy of
-  		            None => error(sy^" not declared") | Some(T) => T;
+                            None => error(sy^" not declared") | Some(T) => T;
            val arity = length (fst (strip_type T));
        in sy ^ (arg_str arity name "") end;
 
   fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");