# HG changeset patch
# User wenzelm
# Date 1270993325 -7200
# Node ID 03aa51cf85a2e659b29459baff231e324f3f45d0
# Parent  2af69e16eced1b83b83ef37cbc32bec6b81cbdcb
stay within Local_Defs layer;

diff -r 2af69e16eced -r 03aa51cf85a2 src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Sun Apr 11 15:22:15 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sun Apr 11 15:42:05 2010 +0200
@@ -64,7 +64,7 @@
   val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
   val (_, prop') = Local_Defs.cert_def lthy prop
-  val (_, newrhs) = Primitive_Defs.abs_def prop'
+  val (_, newrhs) = Local_Defs.abs_def prop'
 
   val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy