--- 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;