--- a/src/HOL/Tools/res_clause.ML Thu Dec 14 22:19:39 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML Fri Dec 15 00:08:06 2006 +0100
@@ -745,7 +745,7 @@
val clss = conjectures @ axclauses
val funcs = funcs_of_clauses clss arity_clauses
and preds = preds_of_clauses clss classrel_clauses arity_clauses
- and probname = Path.pack (Path.base (Path.unpack filename))
+ and probname = Path.implode (Path.base (Path.explode filename))
val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
val tfree_clss = map dfg_tfree_clause (union_all tfree_litss)
val out = TextIO.openOut filename