--- a/src/Pure/Isar/proof_context.ML Fri Jul 15 22:17:09 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Jul 15 22:23:36 2016 +0200
@@ -262,10 +262,6 @@
fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
(mode, syntax, tsig, consts, facts, cases));
-fun map_mode f =
- map_data (fn (Mode {pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
- (make_mode (f (pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
-
fun map_syntax f =
map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
(mode, f syntax, tsig, consts, facts, cases));