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