diff -r b3235bd87da7 -r 7a9cda53bfa2 src/HOL/Tools/ATP/recon_parse.ML
--- a/src/HOL/Tools/ATP/recon_parse.ML	Tue Jun 21 21:41:08 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML	Tue Jun 21 23:44:18 2005 +0200
@@ -209,16 +209,24 @@
 				  then 
 				      nums
 				  else
-			          let val num = hd rest
-                                      val int_of = num_int num
-	
+			          let val first = hd rest
+				
 			          in
-				     linenums rest (int_of::nums)
+				    if (first = (Other "*") ) 
+				    then 
+					
+					 linenums rest ((num_int (hd (tl rest)))::nums)
+				     else
+					  linenums rest ((num_int first)::nums)
 			         end
                                 end
 
-fun get_linenums proofstr = let val s = extract_proof proofstr
-                                val tokens = #1(lex s)
+
+(* This relies on a Vampire proof line starting "% Number" or "% * Number"*)
+(* Check this is right *)
+
+fun get_linenums proofstr = let (*val s = extract_proof proofstr*)
+                                val tokens = #1(lex proofstr)
 	                 
 	                    in
 		                rev (linenums tokens [])