src/HOL/Tools/Quotient/quotient_def.ML
changeset 45797 977cf00fb8d3
parent 45598 87a2624f57e4
child 45826 67110d6c66de
     1.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Dec 09 14:12:02 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Dec 09 14:14:37 2011 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4            else error_msg binding lhs_str
     1.5        | _ => raise Match)
     1.6  
     1.7 -    val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
     1.8 +    val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs
     1.9      val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
    1.10      val (_, prop') = Local_Defs.cert_def lthy prop
    1.11      val (_, newrhs) = Local_Defs.abs_def prop'