# HG changeset patch
# User blanchet
# Date 1269794367 -7200
# Node ID eb44a5d40b9ef673698789f383344db82813abbe
# Parent  f4f34350024925abf2672fca574066317605dbae
make SML/NJ happy

diff -r f4f343500249 -r eb44a5d40b9e src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Mar 28 17:43:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Mar 28 18:39:27 2010 +0200
@@ -28,9 +28,10 @@
 fun only_relevance_override ns : relevance_override =
   {add = ns, del = [], only = true}
 val default_relevance_override = add_to_relevance_override []
-fun merge_relevance_override_pairwise r1 r2 : relevance_override =
+fun merge_relevance_override_pairwise (r1 : relevance_override)
+                                      (r2 : relevance_override) =
   {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
-   only = #only r1 orelse #only r2} 
+   only = #only r1 orelse #only r2}
 fun merge_relevance_overrides rs =
   fold merge_relevance_override_pairwise rs default_relevance_override