--- 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