tuned;

--- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 25 16:55:32 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 25 18:24:49 2012 +0200
@@ -275,7 +275,7 @@
 fun cmts (t1 :: t2 :: toks) =
       if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
       else cmts (t2 :: toks)
-  | cmts toks = [];
+  | cmts _ = [];
 
 in
 

--- a/src/Tools/subtyping.ML	Tue Sep 25 16:55:32 2012 +0200
+++ b/src/Tools/subtyping.ML	Tue Sep 25 18:24:49 2012 +0200
@@ -950,9 +950,10 @@
             if member (op aconv) ts t then (a, b) :: pairs else pairs) tab [(a, b)];
         fun delete pair (G, tab) = (Graph.del_edge pair G, Symreltab.delete_safe pair tab);
         val (G', tab') = fold delete pairs (G, tab);
-        fun reinsert pair (G, xs) = (case (Graph.irreducible_paths G pair) of
-              [] => (G, xs)
-            | _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs));
+        fun reinsert pair (G, xs) =
+          (case Graph.irreducible_paths G pair of
+            [] => (G, xs)
+          | _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs));
         val (G'', ins) = fold reinsert pairs (G', []);
       in
         (fold Symreltab.update ins tab', G'', restrict_graph G'')