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_def.ML
changeset 59157 949829bae42a
parent 57960 ee1ba4848896
child 59580 cbc38731d42f 
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Dec 19 21:24:59 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Dec 19 21:59:18 2014 +0100
@@ -81,7 +81,7 @@
         (fn phi =>
           (case Quotient_Info.transform_quotconsts phi qconst_data of
             qcinfo as {qconst = Const (c, _), ...} =>
-              Quotient_Info.update_quotconsts c qcinfo
+              Quotient_Info.update_quotconsts (c, qcinfo)
           | _ => I))
       |> (snd oo Local_Theory.note) 
         ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
isabelle