author | wenzelm |
Fri, 20 Mar 2015 19:05:03 +0100 | |
changeset 59767 | 745f5e43cf92 |
parent 59766 | 9c99e5f9fb5e |
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);