--- a/Quot/QuotMain.thy	Tue Dec 08 22:02:14 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 22:24:24 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotMain
-imports QuotScript QuotProd Prove
+imports QuotScript Prove
 uses ("quotient_info.ML")
      ("quotient.ML")
      ("quotient_def.ML")
@@ -142,22 +142,19 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
-declare [[map * = (prod_fun, prod_rel)]]
+
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 (* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 
-lemmas [quot_thm] =
-  fun_quotient prod_quotient
+lemmas [quot_thm] = fun_quotient 
 
-lemmas [quot_respect] =
-  quot_rel_rsp pair_rsp
+lemmas [quot_respect] = quot_rel_rsp
 
 (* fun_map is not here since equivp is not true *)
 (* TODO: option, ... *)
-lemmas [quot_equiv] =
-  identity_equivp prod_equivp
+lemmas [quot_equiv] = identity_equivp
 
 (* definition of the quotient types *)
 (* FIXME: should be called quotient_typ.ML *)
@@ -1056,12 +1053,13 @@
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
       (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
-    val thms1 = @{thms all_prs ex_prs} @ defs
-    val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
+    val thms1 = defs @ (prs_rules_get lthy)
+    val thms2 = @{thms fun_map.simps Quotient_abs_rep Quotient_rel_rep babs_prs all_prs ex_prs} 
+                @ (id_simps_get lthy)
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
-    EVERY' [lambda_prs_tac lthy,
-            simp_tac (simps thms1),
+    EVERY' [simp_tac (simps thms1),
+            lambda_prs_tac lthy,
             simp_tac (simps thms2),
             lambda_prs_tac lthy,
             TRY o rtac refl]