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