# HG changeset patch # User blanchet # Date 1346925079 -7200 # Node ID f9d48d479c843f53d35ab1bff9c10459ddb4bb10 # Parent 84e3ad0d64beaa2d37644f972775d672c7956383 don't throw away the context when hacking the theory (first step to localize the sugar code) diff -r 84e3ad0d64be -r f9d48d479c84 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- 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;