# HG changeset patch
# User blanchet
# Date 1398245379 -7200
# Node ID 558afd4292554c9525265dacb56e3f1182a37b97
# Parent  7f9b686bf30a3c3d0e56c8888775d7754a62a87e
made SML/NJ happier

diff -r 7f9b686bf30a -r 558afd429255 src/HOL/Tools/BNF/bnf_def.ML
--- 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}
diff -r 7f9b686bf30a -r 558afd429255 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- 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, _), ...} =>
diff -r 7f9b686bf30a -r 558afd429255 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- 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}