--- a/src/HOL/Tools/res_reconstruct.ML Sat Sep 12 16:30:48 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Sun Sep 13 02:07:06 2009 +0200
@@ -523,7 +523,7 @@
let
val last_axiom = Vector.length thm_names
fun is_axiom n = n <= last_axiom
- fun is_conj n = n >= #1 conj_count andalso n < #1 conj_count + #2 conj_count
+ fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
fun getname i = Vector.sub(thm_names, i-1)
in
(sort_distinct string_ord (filter (fn x => x <> "??.unknown")