changeset 53040 | e6edd7abc4ce |
parent 53039 | 476db75906ae |
child 53210 | 7219c61796c0 |
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Fri Aug 16 18:56:33 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Fri Aug 16 19:03:31 2013 +0200 @@ -120,7 +120,7 @@ val safe_elim_attrs = @{attributes [elim!]}; val simp_attrs = @{attributes [simp]}; -fun unflat_lookup eq xs ys = map (fn xs' => mk_permute eq xs xs' ys); +fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys); fun mk_half_pairss' _ ([], []) = [] | mk_half_pairss' indent (x :: xs, _ :: ys) =