src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 56522 f54003750e7d
parent 56376 5a93b8f928a2
child 56523 2ae16e3d8b6d
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 10 17:48:16 2014 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4    thy
     1.5    |> Sign.root_path
     1.6    |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
     1.7 -  |> f ctr_sugar
     1.8 +  |> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)
     1.9    |> Sign.restore_naming thy;
    1.10  
    1.11  val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
    1.12 @@ -1019,4 +1019,6 @@
    1.13      (parse_ctr_options -- parse_binding --| @{keyword "for"} -- parse_ctr_specs
    1.14       >> free_constructors_cmd);
    1.15  
    1.16 +val _ = Context.>> (Context.map_theory Ctr_Sugar_Interpretation.init);
    1.17 +
    1.18  end;