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