changeset 33317 | b4534348b8fd |
parent 32784 | 1a5dde5079ac |
child 33368 | b1cf34f1855c |
--- a/src/Pure/Isar/rule_insts.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/Isar/rule_insts.ML Thu Oct 29 17:58:26 2009 +0100 @@ -268,7 +268,7 @@ (* Separate type and term insts *) fun has_type_var ((x, _), _) = (case Symbol.explode x of "'" :: _ => true | _ => false); - val Tinsts = List.filter has_type_var insts; + val Tinsts = filter has_type_var insts; val tinsts = filter_out has_type_var insts; (* Tactic *)