# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID 20f282bb83718e4fcb1aae7577a8ae0f3c16c86c
# Parent  eae296b5ef3305ebc1bcc0592584a060eb644715
have the same no-update semantics for 'case' as for 'Ctr_Sugar' and BNF data (this might not be the final word on the matter, but using a consistent policy seems like a good idea)

diff -r eae296b5ef33 -r 20f282bb8371 src/HOL/Tools/Ctr_Sugar/case_translation.ML
--- a/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Tue Feb 11 12:08:44 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/case_translation.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -221,8 +221,9 @@
     val constr_keys = map (fst o dest_Const) constrs;
     val data = (case_comb, constrs);
     val Tname = Tname_of_data data;
-    val update_constrs = fold (fn key => Symtab.cons_list (key, (Tname, data))) constr_keys;
-    val update_cases = Symtab.update (case_key, data);
+    val update_constrs =
+      fold (fn key => Symtab.insert_list (eq_fst (op =)) (key, (Tname, data))) constr_keys;
+    val update_cases = Symtab.default (case_key, data);
   in
     context
     |> map_constrs update_constrs