--- a/src/Pure/Isar/proof_context.ML Mon Mar 30 22:34:59 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Mar 31 00:11:54 2015 +0200
@@ -1195,7 +1195,7 @@
(Name_Space.del_table name cases, index)
| update_case context is_proper (name, SOME c) (cases, index) =
let
- val binding = Binding.name name |> not is_proper ? Binding.conceal;
+ val binding = Binding.name name |> not is_proper ? Binding.concealed;
val (_, cases') = Name_Space.define context false (binding, ((c, is_proper), index)) cases;
val index' = index + 1;
in (cases', index') end;