| changeset 59767 | 745f5e43cf92 |
| parent 59763 | 56d2c357e6b5 |
| child 59768 | 98b362857580 |
--- 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);