don't throw away the context when hacking the theory (first step to localize the sugar code)

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:46:08 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Thu Sep 06 11:51:19 2012 +0200
@@ -276,12 +276,10 @@
 
 fun data_cmd info specs lthy =
   let
-    val fake_lthy =
-      Proof_Context.theory_of lthy
-      |> Theory.copy
-      |> Sign.add_types_global (map (fn spec =>
-        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of_typ spec)) specs)
-      |> Proof_Context.init_global
+    val fake_thy = Theory.copy
+      #> Sign.add_types_global (map (fn spec =>
+        (type_binder_of spec, length (type_args_constrained_of spec), mixfix_of_typ spec)) specs);
+    val fake_lthy = Proof_Context.background_theory fake_thy lthy;
   in
     prepare_data Syntax.read_typ info specs fake_lthy lthy
   end;