--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 11:29:39 2014 +0200
@@ -1352,7 +1352,7 @@
(*|> Sign.restore_naming thy*)
end;
-val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
+fun bnf_interpretation f = BNF_Interpretation.interpretation (with_repaired_path f);
fun register_bnf key bnf =
Local_Theory.declaration {syntax = false, pervasive = true}
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 11:29:39 2014 +0200
@@ -130,7 +130,7 @@
|> f fp_sugars
(*|> Sign.restore_naming thy*);
-val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
+fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f);
fun register_fp_sugars (fp_sugars as {fp, ...} :: _) =
fold (fn fp_sugar as {T = Type (s, _), ...} =>
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Apr 23 11:29:39 2014 +0200
@@ -166,7 +166,7 @@
(*|> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)*)
(*|> Sign.restore_naming thy*);
-val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
+fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f);
fun register_ctr_sugar key ctr_sugar =
Local_Theory.declaration {syntax = false, pervasive = true}