| changeset 53035 | b139670d88d9 |
| parent 53034 | 6067703399ad |
| child 53037 | e5fa456890b4 |
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 16 18:04:39 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Fri Aug 16 18:06:37 2013 +0200 @@ -177,8 +177,6 @@ val exists_subtype_in = Term.exists_subtype o member (op =); -fun resort_tfree S (TFree (s, _)) = TFree (s, S); - val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs)); fun flat_rec_arg_args xss =