# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261699086 -3600
# Node ID 8237786171f14faea179b0d66c91d6441d2422b8
# Parent  0b60d8416ec569e000f7ee75a128bb847fb70749
tuned

diff -r 0b60d8416ec5 -r 8237786171f1 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Fri Dec 25 00:17:55 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 25 00:58:06 2009 +0100
@@ -90,6 +90,7 @@
 
 end
 
+term Quot_Type.abs
 
 section {* ML setup *}
 
diff -r 0b60d8416ec5 -r 8237786171f1 Quot/quotient_def.ML
--- a/Quot/quotient_def.ML	Fri Dec 25 00:17:55 2009 +0100
+++ b/Quot/quotient_def.ML	Fri Dec 25 00:58:06 2009 +0100
@@ -3,6 +3,7 @@
 sig 
   val quotient_def: mixfix -> Attrib.binding -> term -> term ->
     local_theory -> (term * thm) * local_theory
+
   val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
     local_theory -> local_theory
 end;
diff -r 0b60d8416ec5 -r 8237786171f1 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Dec 25 00:17:55 2009 +0100
+++ b/Quot/quotient_tacs.ML	Fri Dec 25 00:58:06 2009 +0100
@@ -504,18 +504,21 @@
 
 fun clean_tac_aux lthy =
 let
+  (*FIXME produce defs with lthy, like prs and ids *)
   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 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
-  val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) 
-  fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+   (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
+  val prs = prs_rules_get lthy
+  val ids = id_simps_get lthy
+  
+  fun mk_simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
+  val ss1 = mk_simps (defs @ prs @ @{thms babs_prs all_prs ex_prs})
+  val ss2 = mk_simps (@{thms Quotient_abs_rep Quotient_rel_rep} @ ids) 
 in
-  EVERY' [simp_tac (simps thms1),
+  EVERY' [simp_tac ss1,
           fun_map_tac lthy,
           lambda_prs_tac lthy,
-          simp_tac (simps thms2),
+          simp_tac ss2,
           TRY o rtac refl]  
 end
 
diff -r 0b60d8416ec5 -r 8237786171f1 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Fri Dec 25 00:17:55 2009 +0100
+++ b/Quot/quotient_typ.ML	Fri Dec 25 00:58:06 2009 +0100
@@ -1,9 +1,8 @@
 signature QUOTIENT_TYPE =
 sig
-  exception LIFT_MATCH of string
-
   val quotient_type: ((string list * binding * mixfix) * (typ * term)) list 
     -> Proof.context -> Proof.state
+
   val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list 
     -> Proof.context -> Proof.state
 end;
@@ -13,8 +12,6 @@
 
 open Quotient_Info;
 
-exception LIFT_MATCH of string
-
 (* wrappers for define, note, Attrib.internal and theorem_i *)
 fun define (name, mx, rhs) lthy =
 let
@@ -230,7 +227,7 @@
   fun after_qed thms lthy =
     fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
 
-  (* sanity check*)  
+  (* sanity check *)  
   val _ = map sanity_check quot_list 
 in
   theorem after_qed goals lthy