# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277623981 -3600
# Node ID 19fca77829eac43fc82782621bb1422604d6c806
# Parent  1b5bbc4a14bccde1fa5573919efe82c77cf9f1fb
mixfix can be given for automatically lifted constants

diff -r 1b5bbc4a14bc -r 19fca77829ea src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Jun 26 08:23:40 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Jun 27 08:33:01 2010 +0100
@@ -12,7 +12,7 @@
   val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) ->
     local_theory -> Quotient_Info.qconsts_info * local_theory
 
-  val lift_raw_const: typ list -> string * term -> local_theory ->
+  val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
     Quotient_Info.qconsts_info * local_theory
 end;
 
@@ -88,13 +88,13 @@
 end
 
 (* a wrapper for automatically lifting a raw constant *)
-fun lift_raw_const qtys (qconst_name, rconst) ctxt =
+fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
 let
   val rty = fastype_of rconst
   val qty = derive_qtyp qtys rty ctxt
+  val lhs = Free (qconst_name, qty)
 in
-  quotient_def ((NONE, NoSyn), (Attrib.empty_binding,
-    (Free (qconst_name, qty), rconst))) ctxt
+  quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
 end
 
 (* parser and command *)