src/HOL/Tools/res_clause.ML
changeset 21858 05f57309170c
parent 21813 06a06f6d3166
child 22079 b161604f0c8d
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu Dec 14 22:19:39 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Dec 15 00:08:06 2006 +0100
     1.3 @@ -745,7 +745,7 @@
     1.4      val clss = conjectures @ axclauses
     1.5      val funcs = funcs_of_clauses clss arity_clauses
     1.6      and preds = preds_of_clauses clss classrel_clauses arity_clauses
     1.7 -    and probname = Path.pack (Path.base (Path.unpack filename))
     1.8 +    and probname = Path.implode (Path.base (Path.explode filename))
     1.9      val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
    1.10      val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
    1.11      val out = TextIO.openOut filename