diff -r c6c8786b9921 -r e2a721567f67 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Jan 21 13:55:07 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Fri Jan 21 18:00:18 2005 +0100
@@ -662,7 +662,7 @@
 	val knd = string_of_arKind arcls
 	val all_lits = concl_lit :: prems_lits
     in
-	"input_clause(" ^ arcls_id ^ "," ^ knd ^ (ResLib.list_to_string' all_lits) ^ ")."
+	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ (ResLib.list_to_string' all_lits) ^ ")."
 	
     end;
 
@@ -674,7 +674,7 @@
     let val tvar = "(T)"
     in 
 	case sup of None => "[++" ^ sub ^ tvar ^ "]"
-		  | (Some supcls) =>  "[++" ^ sub ^ tvar ^ ",--" ^ supcls ^ tvar ^ "]"
+		  | (Some supcls) =>  "[--" ^ sub ^ tvar ^ ",++" ^ supcls ^ tvar ^ "]"
     end;