equal
deleted
inserted
replaced
202 typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2, |
202 typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2, |
203 types = AList.merge (op =) (K true) (types1, types2), |
203 types = AList.merge (op =) (K true) (types1, types2), |
204 realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2), |
204 realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2), |
205 defs = Library.merge Thm.eq_thm (defs1, defs2), |
205 defs = Library.merge Thm.eq_thm (defs1, defs2), |
206 expand = Library.merge (op =) (expand1, expand2), |
206 expand = Library.merge (op =) (expand1, expand2), |
207 prep = (case prep1 of NONE => prep2 | _ => prep1)}; |
207 prep = if is_some prep1 then prep1 else prep2}; |
208 ); |
208 ); |
209 |
209 |
210 fun read_condeq thy = |
210 fun read_condeq thy = |
211 let val thy' = add_syntax thy |
211 let val thy' = add_syntax thy |
212 in fn s => |
212 in fn s => |