changeset 38761 | b32975d3db3e |
parent 37310 | 96e2b9a6f074 |
child 39288 | f1ae2493d93f |
--- a/src/Pure/Proof/extraction.ML Thu Aug 26 16:56:45 2010 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Aug 26 17:01:12 2010 +0200 @@ -204,7 +204,7 @@ realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2), defs = Library.merge Thm.eq_thm (defs1, defs2), expand = Library.merge (op =) (expand1, expand2), - prep = (case prep1 of NONE => prep2 | _ => prep1)}; + prep = if is_some prep1 then prep1 else prep2}; ); fun read_condeq thy =