add_cases: omit unnamed;
authorwenzelm
Wed Mar 08 23:49:30 2000 +0100 (2000-03-08)
changeset 838413bc74731ae6
parent 8383 2dd4823c744f
child 8385 514df4f1df10
add_cases: omit unnamed;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 08 23:48:34 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 08 23:49:30 2000 +0100
     1.3 @@ -833,8 +833,12 @@
     1.4      None => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
     1.5    | Some c => c);
     1.6  
     1.7 +
     1.8 +fun add_case (tab, ("", _)) = tab
     1.9 +  | add_case (tab, name_c) = Symtab.update (name_c, tab);
    1.10 +
    1.11  fun add_cases xs = map_context (fn (thy, data, asms, binds, thms, cases, defs) =>
    1.12 -  (thy, data, asms, binds, thms, foldl (Symtab.update o swap) (cases, xs), defs));
    1.13 +  (thy, data, asms, binds, thms, foldl add_case (cases, xs), defs));
    1.14  
    1.15  
    1.16