TODO
authorblanchet
Sat, 08 Sep 2012 21:04:26 +0200
changeset 49209 3c0deda51b32
parent 49208 3f73424f86a7
child 49210 656fb50d33f0
TODO
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