--- a/src/Pure/Isar/rule_insts.ML Wed Sep 30 19:04:48 2009 +0200
+++ b/src/Pure/Isar/rule_insts.ML Wed Sep 30 22:20:58 2009 +0200
@@ -266,8 +266,8 @@
let
val thy = ProofContext.theory_of ctxt;
(* Separate type and term insts *)
- fun has_type_var ((x, _), _) = (case Symbol.explode x of
- "'"::cs => true | cs => false);
+ fun has_type_var ((x, _), _) =
+ (case Symbol.explode x of "'" :: _ => true | _ => false);
val Tinsts = List.filter has_type_var insts;
val tinsts = filter_out has_type_var insts;