make SML/NJ happy
authorblanchet
Sun, 28 Mar 2010 18:39:27 +0200
changeset 36003 eb44a5d40b9e
parent 36002 f4f343500249
child 36005 3956a7636d5d
child 36058 8256d5a185bd
make SML/NJ happy
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