src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 56522 f54003750e7d
parent 56521 20cfb18a53ba
child 56523 2ae16e3d8b6d
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
@@ -197,7 +197,7 @@
   thy
   |> Sign.root_path
   |> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))
-  |> f fp_sugar
+  |> (fn thy => f (morph_fp_sugar (Morphism.transfer_morphism thy) fp_sugar) thy)
   |> Sign.restore_naming thy;
 
 val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
@@ -1445,4 +1445,6 @@
 
 fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
 
+val _ = Context.>> (Context.map_theory FP_Sugar_Interpretation.init);
+
 end;