# HG changeset patch
# User blanchet
# Date 1285403534 -7200
# Node ID 6542245db5c2961b0a71f8fb41d716be84bd73b6
# Parent  1906c0c773415542b32e9a88ea2e01d2fef3722d
make SML/NJ happy

diff -r 1906c0c77341 -r 6542245db5c2 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Fri Sep 24 17:55:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sat Sep 25 10:32:14 2010 +0200
@@ -228,8 +228,8 @@
                       | NONE => ~1
   in if k >= 0 then [k] else [] end
 
-val is_axiom = not o null oo resolve_axiom
-val is_conjecture = not o null oo resolve_conjecture
+fun is_axiom conjecture_shape = not o null o resolve_axiom conjecture_shape
+fun is_conjecture conjecture_shape = not o null o resolve_conjecture conjecture_shape
 
 fun raw_label_for_name conjecture_shape name =
   case resolve_conjecture conjecture_shape name of