# HG changeset patch
# User wenzelm
# Date 1468614216 -7200
# Node ID 3b9ab054a3563d7d1f1252b297594d4dd5a1b39d
# Parent  34859964488725f2d5526b08fb73d0c039f901ec
unused;

diff -r 348599644887 -r 3b9ab054a356 src/Pure/Isar/proof_context.ML
--- 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));