made SML/NJ happier
authorblanchet
Wed, 23 Apr 2014 11:29:39 +0200
changeset 56657 558afd429255
parent 56656 7f9b686bf30a
child 56675 140e6d01c481
made SML/NJ happier
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.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}
--- 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}