src/HOL/Quotient.thy
changeset 47094 1a7ad2601cb5
parent 47091 d5cd13aca90b
child 47096 3ea48c19673e
     1.1 --- a/src/HOL/Quotient.thy	Fri Mar 23 14:18:43 2012 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Fri Mar 23 14:20:09 2012 +0100
     1.3 @@ -686,8 +686,7 @@
     1.4  use "Tools/Quotient/quotient_info.ML"
     1.5  setup Quotient_Info.setup
     1.6  
     1.7 -declare [[map "fun" = fun_rel]]
     1.8 -declare [[map set = set_rel]]
     1.9 +declare [[map "fun" = (fun_rel, fun_quotient)]]
    1.10  
    1.11  lemmas [quot_thm] = fun_quotient
    1.12  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp