# HG changeset patch
# User wenzelm
# Date 952555770 -3600
# Node ID 13bc74731ae6c1fdd48870472a4b3c2b536de086
# Parent  2dd4823c744f0dae11565fe825e18a50718011ad
add_cases: omit unnamed;

diff -r 2dd4823c744f -r 13bc74731ae6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Mar 08 23:48:34 2000 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 08 23:49:30 2000 +0100
@@ -833,8 +833,12 @@
     None => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
   | Some c => c);
 
+
+fun add_case (tab, ("", _)) = tab
+  | add_case (tab, name_c) = Symtab.update (name_c, tab);
+
 fun add_cases xs = map_context (fn (thy, data, asms, binds, thms, cases, defs) =>
-  (thy, data, asms, binds, thms, foldl (Symtab.update o swap) (cases, xs), defs));
+  (thy, data, asms, binds, thms, foldl add_case (cases, xs), defs));