tuned ctr_sugar database handling
authorblanchet
Wed, 03 Sep 2014 22:47:48 +0200
changeset 58176 710710a66173
parent 58175 2412a3369c30
child 58177 166131276380
tuned ctr_sugar database handling
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