# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259936406 -3600
# Node ID 53984a386999b866453d75c07135fbfae1163c05
# Parent  3feed4dbfa458d976dc46b280a71c6efb0a7198a# Parent  6348c2a57ec2e2168f246ba0fe2bffcfde965d45
merged

diff -r 6348c2a57ec2 -r 53984a386999 LFex.thy
--- a/LFex.thy	Fri Dec 04 15:18:33 2009 +0100
+++ b/LFex.thy	Fri Dec 04 15:20:06 2009 +0100
@@ -219,7 +219,7 @@
 ML {*
   val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
   val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
-  val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot
+  (*val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}*)
   val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
   val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
 *}
diff -r 6348c2a57ec2 -r 53984a386999 QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 15:18:33 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 15:20:06 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotScript
-imports Main
+imports Plain ATP_Linkup
 begin
 
 definition 
diff -r 6348c2a57ec2 -r 53984a386999 quotient_def.ML
--- a/quotient_def.ML	Fri Dec 04 15:18:33 2009 +0100
+++ b/quotient_def.ML	Fri Dec 04 15:20:06 2009 +0100
@@ -118,7 +118,7 @@
 let   
   val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, rhs) = Primitive_Defs.abs_def prop'
-in
+in  
   make_def bind qty mx attr rhs lthy 
 end