1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 10 17:48:16 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Apr 10 17:48:16 2014 +0200
     1.3 @@ -1326,7 +1326,7 @@
     1.4      thy
     1.5      |> Sign.root_path
     1.6      |> fold (uncurry (fn true => Sign.mandatory_path | false => Sign.add_path) o swap) qualifiers
     1.7 -    |> f bnf
     1.8 +    |> (fn thy => f (morph_bnf (Morphism.transfer_morphism thy) bnf) thy)
     1.9      |> Sign.restore_naming thy
    1.10    end;
    1.11  
    1.12 @@ -1422,4 +1422,6 @@
    1.13         Scan.option ((Parse.reserved "rel" -- @{keyword ":"}) |-- Parse.term)
    1.14         >> bnf_cmd);
    1.15  
    1.16 +val _ = Context.>> (Context.map_theory BNF_Interpretation.init);
    1.17 +
    1.18  end;

     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
     2.3 @@ -197,7 +197,7 @@
     2.4    thy
     2.5    |> Sign.root_path
     2.6    |> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))
     2.7 -  |> f fp_sugar
     2.8 +  |> (fn thy => f (morph_fp_sugar (Morphism.transfer_morphism thy) fp_sugar) thy)
     2.9    |> Sign.restore_naming thy;
    2.10  
    2.11  val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
    2.12 @@ -1445,4 +1445,6 @@
    2.13  
    2.14  fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
    2.15  
    2.16 +val _ = Context.>> (Context.map_theory FP_Sugar_Interpretation.init);
    2.17 +
    2.18  end;

     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
     3.3 @@ -162,7 +162,7 @@
     3.4    thy
     3.5    |> Sign.root_path
     3.6    |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
     3.7 -  |> f ctr_sugar
     3.8 +  |> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)
     3.9    |> Sign.restore_naming thy;
    3.10  
    3.11  val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
    3.12 @@ -1019,4 +1019,6 @@
    3.13      (parse_ctr_options -- parse_binding --| @{keyword "for"} -- parse_ctr_specs
    3.14       >> free_constructors_cmd);
    3.15  
    3.16 +val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);
    3.17 +
    3.18  end;