| changeset 47777 | f29e7dcd7c40 |
| parent 47698 | 18202d3d5832 |
| child 47889 | 29212a4bb866 |
--- a/src/HOL/Lifting.thy Thu Apr 26 01:05:06 2012 +0200 +++ b/src/HOL/Lifting.thy Thu Apr 26 12:01:58 2012 +0200 @@ -360,7 +360,7 @@ use "Tools/Lifting/lifting_info.ML" setup Lifting_Info.setup -declare [[map "fun" = (fun_rel, fun_quotient)]] +declare fun_quotient[quot_map] use "Tools/Lifting/lifting_term.ML"