--- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 11:08:21 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 12:33:51 2010 +0100
@@ -84,7 +84,7 @@
*)
fun mk_mapfun ctxt vs rty =
let
- val vs' = map (mk_Free) vs
+ val vs' = map mk_Free vs
fun mk_mapfun_aux rty =
case rty of
@@ -103,7 +103,7 @@
let
val thy = ProofContext.theory_of ctxt
val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
- val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
+ val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn
in
(#rtyp qdata, #qtyp qdata)
end