1.1 --- a/src/Pure/Proof/extraction.ML	Thu Aug 26 16:56:45 2010 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Aug 26 17:01:12 2010 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4       realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
     1.5       defs = Library.merge Thm.eq_thm (defs1, defs2),
     1.6       expand = Library.merge (op =) (expand1, expand2),
     1.7 -     prep = (case prep1 of NONE => prep2 | _ => prep1)};
     1.8 +     prep = if is_some prep1 then prep1 else prep2};
     1.9  );
    1.10  
    1.11  fun read_condeq thy =