# HG changeset patch
# User kuncar
# Date 1397144896 -7200
# Node ID f54003750e7d123cf1e32efa36c9f2839f42afc4
# Parent  20cfb18a53ba1d625071ad6b8cd399ef6ba5d3d1
don't forget to init Interpretation and transfer theorems in the interpretation hook

diff -r 20cfb18a53ba -r f54003750e7d src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 10 17:48:16 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 10 17:48:16 2014 +0200
@@ -1326,7 +1326,7 @@
     thy
     |> Sign.root_path
     |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
-    |> f bnf
+    |> (fn thy => f (morph_bnf (Morphism.transfer_morphism thy) bnf) thy)
     |> Sign.restore_naming thy
   end;
 
@@ -1422,4 +1422,6 @@
        Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term)
        >> bnf_cmd);
 
+val _ = Context.>> (Context.map_theory BNF_Interpretation.init);
+
 end;
diff -r 20cfb18a53ba -r f54003750e7d src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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;
diff -r 20cfb18a53ba -r f54003750e7d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
@@ -162,7 +162,7 @@
   thy
   |> Sign.root_path
   |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
-  |> f ctr_sugar
+  |> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)
   |> Sign.restore_naming thy;
 
 val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
@@ -1019,4 +1019,6 @@
     (parse_ctr_options -- parse_binding --| @{keyword "for"} -- parse_ctr_specs
      >> free_constructors_cmd);
 
+val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);
+
 end;