--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 16 16:48:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 16 18:04:39 2013 +0200
@@ -179,14 +179,6 @@
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)
- | SOME T' => T')
- | typ_subst_nonatomic inst T = the_default T (AList.lookup (op =) inst T);
-
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
fun flat_rec_arg_args xss =