--- 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, _), ...} =>