# HG changeset patch
# User blanchet
# Date 1376481954 -7200
# Node ID 8444e1b8e7a384835774161d75816fe4dfb3532e
# Parent  a1e64c804c35e281d6cf799aee8c684a4e64f87e
added fixme

diff -r a1e64c804c35 -r 8444e1b8e7a3 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 14 13:15:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 14 14:05:54 2013 +0200
@@ -177,6 +177,8 @@
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
 
+(* FIXME: merge with function of the same name in "bnf_fp_n2m.ML" (in the
+   prim(co)rec repository) *)
 fun typ_subst_nonatomic inst (T as Type (s, Ts)) =
     (case AList.lookup (op =) inst T of
       NONE => Type (s, map (typ_subst_nonatomic inst) Ts)