diff -r 4e5a43b0e7dd -r bfde04fc5190 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Sep 01 16:17:47 2014 +0200
@@ -36,7 +36,7 @@
      case_eq_ifs: thm list};
 
   val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
-  val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar
+  val transfer_ctr_sugar: theory -> ctr_sugar -> ctr_sugar
   val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
   val ctr_sugars_of: Proof.context -> ctr_sugar list
   val ctr_sugar_of_case: Proof.context -> string -> ctr_sugar option
@@ -138,8 +138,7 @@
    split_sel_asms = map (Morphism.thm phi) split_sel_asms,
    case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
 
-val transfer_ctr_sugar =
-  morph_ctr_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
+val transfer_ctr_sugar = morph_ctr_sugar o Morphism.transfer_morphism;
 
 structure Data = Generic_Data
 (
@@ -151,10 +150,11 @@
 
 fun ctr_sugar_of ctxt =
   Symtab.lookup (Data.get (Context.Proof ctxt))
-  #> Option.map (transfer_ctr_sugar ctxt);
+  #> Option.map (transfer_ctr_sugar (Proof_Context.theory_of ctxt));
 
 fun ctr_sugars_of ctxt =
-  Symtab.fold (cons o transfer_ctr_sugar ctxt o snd) (Data.get (Context.Proof ctxt)) [];
+  Symtab.fold (cons o transfer_ctr_sugar (Proof_Context.theory_of ctxt) o snd)
+    (Data.get (Context.Proof ctxt)) [];
 
 fun ctr_sugar_of_case ctxt s =
   find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false) (ctr_sugars_of ctxt);