1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Apr 23 10:23:27 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Apr 23 11:29:39 2014 +0200
     1.3 @@ -1352,7 +1352,7 @@
     1.4      (*|> Sign.restore_naming thy*)
     1.5    end;
     1.6  
     1.7 -val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
     1.8 +fun bnf_interpretation f = BNF_Interpretation.interpretation (with_repaired_path f);
     1.9  
    1.10  fun register_bnf key bnf =
    1.11    Local_Theory.declaration {syntax = false, pervasive = true}

     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 23 11:29:39 2014 +0200
     2.3 @@ -130,7 +130,7 @@
     2.4    |> f fp_sugars
     2.5    (*|> Sign.restore_naming thy*);
     2.6  
     2.7 -val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
     2.8 +fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f);
     2.9  
    2.10  fun register_fp_sugars (fp_sugars as {fp, ...} :: _) =
    2.11    fold (fn fp_sugar as {T = Type (s, _), ...} =>

     3.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Apr 23 10:23:27 2014 +0200
     3.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Apr 23 11:29:39 2014 +0200
     3.3 @@ -166,7 +166,7 @@
     3.4    (*|> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)*)
     3.5    (*|> Sign.restore_naming thy*);
     3.6  
     3.7 -val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
     3.8 +fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f);
     3.9  
    3.10  fun register_ctr_sugar key ctr_sugar =
    3.11    Local_Theory.declaration {syntax = false, pervasive = true}