tuned;

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