--- 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;