src/HOL/Lifting.thy
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"