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)