merged
authorwenzelm
Sun, 28 Mar 2010 19:34:08 +0200
changeset 36005 3956a7636d5d
parent 36003 eb44a5d40b9e (diff)
parent 36004 5d79ca55a52b (current diff)
child 36006 7ddc33baf959
child 36069 a15454b23ebd
merged
--- 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