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