# HG changeset patch
# User wenzelm
# Date 1394807212 -3600
# Node ID a200bffe402793f618753a5a03b6ce5fd6690d78
# Parent  27167f903c6d7107370bb5a89a423b25a0f35b45
conceal improper cases, e.g. relevant for completion (and potentially for markup);

diff -r 27167f903c6d -r a200bffe4027 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Mar 14 15:12:22 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Mar 14 15:26:52 2014 +0100
@@ -1167,8 +1167,11 @@
       (Name_Space.del_table name cases, index)
   | update_case context is_proper (name, SOME c) (cases, index) =
       let
-        val (_, cases') = cases |> Name_Space.define context false
-          (Binding.make (name, Position.none), ((c, is_proper), index));
+        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 index' = index + 1;
       in (cases', index') end;