# HG changeset patch
# User wenzelm
# Date 1426874703 -3600
# Node ID 745f5e43cf928bb39f79f2857b23ceb6f64aa529
# Parent  9c99e5f9fb5e7050d0c22322ea33f40292fd4530
make SML/NJ happy;

diff -r 9c99e5f9fb5e -r 745f5e43cf92 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Fri Mar 20 16:18:20 2015 +0000
+++ b/src/Pure/Tools/rule_insts.ML	Fri Mar 20 19:05:03 2015 +0100
@@ -36,7 +36,8 @@
 
 (** reading instantiations **)
 
-val partition_insts = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x);
+fun partition_insts mixed_insts =
+  List.partition (fn (((x, _), _), _) => String.isPrefix "'" x) mixed_insts;
 
 fun error_var msg (xi, pos) =
   error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);