src/CCL/CCL.ML
changeset 3935 52c14fe8f16b
parent 3837 d7f033c74b38
child 4347 d683b7898c61
equal deleted inserted replaced
3934:a9c8960e4da6 3935:52c14fe8f16b
    85   fun saturate thy sy name = 
    85   fun saturate thy sy name = 
    86        let fun arg_str 0 a s = s
    86        let fun arg_str 0 a s = s
    87          | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
    87          | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
    88          | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
    88          | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
    89            val sg = sign_of thy;
    89            val sg = sign_of thy;
    90            val T = case Sign.const_type sg sy of
    90            val T = case Sign.const_type sg (Sign.intern_const (sign_of thy) sy) of
    91                             None => error(sy^" not declared") | Some(T) => T;
    91                             None => error(sy^" not declared") | Some(T) => T;
    92            val arity = length (fst (strip_type T));
    92            val arity = length (fst (strip_type T));
    93        in sy ^ (arg_str arity name "") end;
    93        in sy ^ (arg_str arity name "") end;
    94 
    94 
    95   fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");
    95   fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");