tuned;

--- a/src/Pure/Concurrent/event_timer.ML	Sun Jan 24 14:57:42 2016 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Sun Jan 24 14:58:56 2016 +0100
@@ -110,7 +110,7 @@
 
 fun shutdown () =
   uninterruptible (fn restore_attributes => fn () =>
-    if Synchronized.change_result state (fn st as State {requests, status, manager} =>
+    if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
       if is_shutdown Normal st then (false, st)
       else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
         raise Fail "Concurrent attempt to shutdown event timer"

--- a/src/Pure/General/symbol_pos.ML	Sun Jan 24 14:57:42 2016 +0100
+++ b/src/Pure/General/symbol_pos.ML	Sun Jan 24 14:58:56 2016 +0100
@@ -71,7 +71,7 @@
         fun split syms =
           (case take_prefix (fn (s, _) => s <> "\n") syms of
             (line, []) => [line]
-          | (line, nl :: rest) => line :: split rest);
+          | (line, _ :: rest) => line :: split rest);
       in split list end;
 
 val trim_blanks = trim (Symbol.is_blank o symbol);

--- a/src/Pure/Isar/named_target.ML	Sun Jan 24 14:57:42 2016 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Jan 24 14:58:56 2016 +0100
@@ -86,7 +86,7 @@
   | abbrev (locale, false) = Generic_Target.locale_abbrev locale
   | abbrev (class, true) = Class.abbrev class;
 
-fun declaration ("", _) flags decl = Generic_Target.theory_declaration decl
+fun declaration ("", _) _ decl = Generic_Target.theory_declaration decl
   | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
 
 fun theory_registration ("", _) = Generic_Target.theory_registration

--- a/src/Pure/Isar/toplevel.ML	Sun Jan 24 14:57:42 2016 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Jan 24 14:58:56 2016 +0100
@@ -212,10 +212,6 @@
 fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE)
   | reset_presentation node = node;
 
-fun map_theory f (Theory (gthy, ctxt)) =
-      Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt)
-  | map_theory _ node = node;
-
 in
 
 fun apply_transaction f g node =

--- a/src/Pure/Syntax/syntax_phases.ML	Sun Jan 24 14:57:42 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Jan 24 14:58:56 2016 +0100
@@ -581,7 +581,7 @@
             (mark Ts t1 $ mark Ts t2);
   in mark [] tm end;
 
-fun prune_types ctxt tm =
+fun prune_types tm =
   let
     fun regard t t' seen =
       if Type_Annotation.is_omitted (Type_Annotation.fastype_of [] t) then (t, seen)
@@ -651,7 +651,7 @@
           in Ast.mk_appl (constrain (c $ Syntax.free x) X) (map ast_of ts) end
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (constrain (Syntax.const "_idtdummy") T) (map ast_of ts)
-      | (const as Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
+      | (Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
 
     and trans a T args = ast_of (trf a ctxt T args)
@@ -672,7 +672,7 @@
   in
     tm
     |> mark_aprop
-    |> show_types ? prune_types ctxt
+    |> show_types ? prune_types
     |> Variable.revert_bounds ctxt
     |> mark_atoms is_syntax_const ctxt
     |> ast_of