# HG changeset patch
# User wenzelm
# Date 1433707490 -7200
# Node ID 8111a4d538ec95e7f30958a645b6686fc3efdff0
# Parent  b568b98fa00086c09c378cd377162786251bb56f
tuned (see also 66e6c539a36d);

diff -r b568b98fa000 -r 8111a4d538ec src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jun 07 21:58:18 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Jun 07 22:04:50 2015 +0200
@@ -254,10 +254,7 @@
     (mode, f syntax, tsig, consts, facts, cases));
 
 fun map_syntax_idents f ctxt =
-  let
-    val idents = Syntax_Trans.get_idents ctxt;
-    val (opt_idents', syntax') = f (#syntax (rep_data ctxt));
-  in
+  let val (opt_idents', syntax') = f (#syntax (rep_data ctxt)) in
     ctxt
     |> map_syntax (K syntax')
     |> (case opt_idents' of NONE => I | SOME idents' => Syntax_Trans.put_idents idents')