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 37563 6cf28a1dfd75
parent 37562 21ab339715cd
child 37564 a47bb386b238 
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jun 28 07:32:51 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Mon Jun 28 07:38:39 2010 +0200
@@ -91,7 +91,7 @@
 fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
 let
   val rty = fastype_of rconst
-  val qty = derive_qtyp qtys rty ctxt
+  val qty = derive_qtyp qtys rty false ctxt
   val lhs = Free (qconst_name, qty)
 in
   quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
isabelle