src/HOL/Quotient.thy
changeset 45802 b16f976db515
parent 45782 f82020ca3248
child 45961 5cefe17916a6
     1.1 --- a/src/HOL/Quotient.thy	Fri Dec 09 16:08:32 2011 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Fri Dec 09 18:07:04 2011 +0100
     1.3 @@ -671,8 +671,8 @@
     1.4  use "Tools/Quotient/quotient_info.ML"
     1.5  setup Quotient_Info.setup
     1.6  
     1.7 -declare [[map "fun" = (map_fun, fun_rel)]]
     1.8 -declare [[map set = (vimage, set_rel)]]
     1.9 +declare [[map "fun" = fun_rel]]
    1.10 +declare [[map set = set_rel]]
    1.11  
    1.12  lemmas [quot_thm] = fun_quotient
    1.13  lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp