Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Quotient/quotient_term.ML
changeset 37564 a47bb386b238
parent 37563 6cf28a1dfd75
child 37591 d3daea901123 
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 07:38:39 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 09:48:36 2010 +0200
@@ -759,9 +759,9 @@
      |> map (fn (x, y) => if reverse then (y, x) else (x, y))
 
   val rel_substs =
-    if reverse then [] else
     Quotient_Info.quotdata_dest ctxt
      |> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x)))
+     |> map (fn (x, y) => if reverse then (y, x) else (x, y))
 in
   filter proper (const_substs @ rel_substs)
 end
isabelle