equal
deleted
inserted
replaced
277 (timer; lthy'') |
277 (timer; lthy'') |
278 end; |
278 end; |
279 |
279 |
280 fun data_cmd info specs lthy = |
280 fun data_cmd info specs lthy = |
281 let |
281 let |
|
282 (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a |
|
283 locale and shadows an existing global type*) |
282 val fake_thy = Theory.copy |
284 val fake_thy = Theory.copy |
283 #> fold (fn spec => Sign.add_type lthy |
285 #> fold (fn spec => perhaps (try (Sign.add_type lthy |
284 (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)) specs; |
286 (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs; |
285 val fake_lthy = Proof_Context.background_theory fake_thy lthy; |
287 val fake_lthy = Proof_Context.background_theory fake_thy lthy; |
286 in |
288 in |
287 prepare_data Syntax.read_typ info specs fake_lthy lthy |
289 prepare_data Syntax.read_typ info specs fake_lthy lthy |
288 end; |
290 end; |
289 |
291 |