# HG changeset patch # User blanchet # Date 1347131066 -7200 # Node ID 3c0deda51b3280900ef26cb2c7784bca44928af6 # Parent 3f73424f86a7dc363d17fada60b80c639611aad1 TODO diff -r 3f73424f86a7 -r 3c0deda51b32 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:04:26 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Sat Sep 08 21:04:26 2012 +0200 @@ -391,6 +391,7 @@ fun datatype_cmd info specs lthy = let + (* TODO: cleaner handling of fake contexts, without "background_theory" *) (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a locale and shadows an existing global type*) val fake_thy = Theory.copy