--- 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