# HG changeset patch
# User wenzelm
# Date 1252800426 -7200
# Node ID 5047ab238cc05f873a6111843f3e210e4a93bbf8
# Parent  378528d2f7eb36dd9504b393e0fe61f3d0baf076
made SML/NJ happy;

diff -r 378528d2f7eb -r 5047ab238cc0 src/HOL/Tools/res_reconstruct.ML
--- 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")