# HG changeset patch
# User blanchet
# Date 1409777268 -7200
# Node ID 710710a66173446fe9fecf1e3033a9160ac5dc5c
# Parent  2412a3369c3021b7210edf785f5b58012e4b95e5
tuned ctr_sugar database handling

diff -r 2412a3369c30 -r 710710a66173 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 03 22:47:35 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Sep 03 22:47:48 2014 +0200
@@ -180,7 +180,7 @@
   thy
   |> Sign.root_path
   |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
-  |> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)
+  |> (fn thy => f (transfer_ctr_sugar thy ctr_sugar) thy)
   |> Sign.restore_naming thy;
 
 fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f);
@@ -188,7 +188,8 @@
 fun register_ctr_sugar key ctr_sugar =
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)))
-  #> Local_Theory.background_theory (Ctr_Sugar_Interpretation.data ctr_sugar);
+  #> Local_Theory.background_theory
+    (fn thy => Ctr_Sugar_Interpretation.data (the (ctr_sugar_of_global thy key)) thy);
 
 fun default_register_ctr_sugar_global key ctr_sugar thy =
   let val tab = Data.get (Context.Theory thy) in