# HG changeset patch
# User wenzelm
# Date 1269797648 -7200
# Node ID 3956a7636d5de10e1d90d5b1b28850622c3b2318
# Parent  eb44a5d40b9ef673698789f383344db82813abbe# Parent  5d79ca55a52b70030a16935eb2b5b34e295da2ce
merged

diff -r 5d79ca55a52b -r 3956a7636d5d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Mar 28 19:20:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Mar 28 19:34:08 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