--- a/src/HOL/Import/replay.ML Fri Sep 16 20:30:44 2005 +0200
+++ b/src/HOL/Import/replay.ML Fri Sep 16 21:02:15 2005 +0200
@@ -284,7 +284,7 @@
fun get_facts facts =
case TextIO.inputLine is of
"" => (case facts of
- i::facts => (valOf (Int.fromString i),rev facts)
+ i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
| _ => raise ERR "replay_thm" "Bad facts.lst file")
| fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
in
@@ -340,4 +340,4 @@
replay_fact (thmname,thy)
end
-end
+end
\ No newline at end of file