src/HOL/Import/replay.ML
changeset 17440 df77edc4f5d0
parent 17322 781abf7011e6
child 17592 ece268908438
     1.1 --- a/src/HOL/Import/replay.ML	Fri Sep 16 20:30:44 2005 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Sep 16 21:02:15 2005 +0200
     1.3 @@ -284,7 +284,7 @@
     1.4  		fun get_facts facts =
     1.5  		    case TextIO.inputLine is of
     1.6  			"" => (case facts of
     1.7 -				   i::facts => (valOf (Int.fromString i),rev facts)
     1.8 +				   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
     1.9  				 | _ => raise ERR "replay_thm" "Bad facts.lst file")
    1.10  		      | fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
    1.11  	    in
    1.12 @@ -340,4 +340,4 @@
    1.13  	replay_fact (thmname,thy)
    1.14      end
    1.15  
    1.16 -end
    1.17 +end
    1.18 \ No newline at end of file