src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 53029 8444e1b8e7a3
parent 52969 f2df0730f8ac
child 53031 83cbe188855a
--- 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)