src/Pure/Isar/rule_insts.ML
changeset 32784 1a5dde5079ac
parent 31977 e03059ae2d82
child 33317 b4534348b8fd
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Wed Sep 30 19:04:48 2009 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Wed Sep 30 22:20:58 2009 +0200
     1.3 @@ -266,8 +266,8 @@
     1.4    let
     1.5      val thy = ProofContext.theory_of ctxt;
     1.6      (* Separate type and term insts *)
     1.7 -    fun has_type_var ((x, _), _) = (case Symbol.explode x of
     1.8 -          "'"::cs => true | cs => false);
     1.9 +    fun has_type_var ((x, _), _) =
    1.10 +      (case Symbol.explode x of "'" :: _ => true | _ => false);
    1.11      val Tinsts = List.filter has_type_var insts;
    1.12      val tinsts = filter_out has_type_var insts;
    1.13