Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added fixme
authorblanchet
Wed, 14 Aug 2013 14:05:54 +0200
changeset 53029 8444e1b8e7a3
parent 53028 a1e64c804c35
child 53030 1b18e3ce776f
added fixme
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle