# HG changeset patch # User blanchet # Date 1410288696 -7200 # Node ID 2e91e9bbc2123be16c60a0e814d338e91794dc9b # Parent 16648edf16e3a4767edcea290dfb8cde40f7155d made SML/NJ happier diff -r 16648edf16e3 -r 2e91e9bbc212 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Sep 09 20:51:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Tue Sep 09 20:51:36 2014 +0200 @@ -288,7 +288,7 @@ else ((fp_sugars, (NONE, NONE)), lthy); - fun mk_ctr_of {ctr_sugar = {ctrs, ...}, ...} (Type (_, Ts)) = map (mk_ctr Ts) ctrs; + fun mk_ctr_of ({ctr_sugar = {ctrs, ...}, ...} : fp_sugar) (Type (_, Ts)) = map (mk_ctr Ts) ctrs; val substAT = Term.typ_subst_atomic (var_As ~~ As); val Xs' = map #X fp_sugars';