# HG changeset patch
# User wenzelm
# Date 1408528299 -7200
# Node ID 14c8269d0de9acff78a9a045d6282917ceb51397
# Parent  0b0519c412291150e41ca64c31333c77b86a3d46
tuned;

diff -r 0b0519c41229 -r 14c8269d0de9 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 20 11:05:41 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Aug 20 11:51:39 2014 +0200
@@ -1184,11 +1184,8 @@
       (Name_Space.del_table name cases, index)
   | update_case context is_proper (name, SOME c) (cases, index) =
       let
-        val binding =
-          Binding.make (name, Position.none)
-          |> not is_proper ? Binding.conceal;
-        val (_, cases') = cases
-          |> Name_Space.define context false (binding, ((c, is_proper), index));
+        val binding = Binding.name name |> not is_proper ? Binding.conceal;
+        val (_, cases') = Name_Space.define context false (binding, ((c, is_proper), index)) cases;
         val index' = index + 1;
       in (cases', index') end;