--- a/FSet.thy	Tue Dec 01 12:16:45 2009 +0100
+++ b/FSet.thy	Tue Dec 01 14:04:00 2009 +0100
@@ -523,4 +523,7 @@
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 done
 
+ML {* #quot_thm (hd (quotdata_dest @{theory})) *}
+print_quotients
+thm QUOTIENT_fset
 end

--- a/QuotMain.thy	Tue Dec 01 12:16:45 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 14:04:00 2009 +0100
@@ -260,49 +260,6 @@
 *}
 
 
-section {*  Infrastructure about definitions *}
-
-(* Does the same as 'subst' in a given theorem *)
-ML {*
-fun eqsubst_thm ctxt thms thm =
-  let
-    val goalstate = Goal.init (Thm.cprop_of thm)
-    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
-      NONE => error "eqsubst_thm"
-    | SOME th => cprem_of th 1
-    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
-    val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
-    val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
-    val rt = Goal.prove_internal [] cgoal (fn _ => tac);
-  in
-    @{thm equal_elim_rule1} OF [rt, thm]
-  end
-*}
-
-(* expects atomized definitions *)
-ML {*
-fun add_lower_defs_aux lthy thm =
-  let
-    val e1 = @{thm fun_cong} OF [thm];
-    val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
-    val g = simp_ids f
-  in
-    (simp_ids thm) :: (add_lower_defs_aux lthy g)
-  end
-  handle _ => [simp_ids thm]
-*}
-
-ML {*
-fun add_lower_defs lthy def =
-  let
-    val def_pre_sym = symmetric def
-    val def_atom = atomize_thm def_pre_sym
-    val defs_all = add_lower_defs_aux lthy def_atom
-  in
-    map Thm.varifyT defs_all
-  end
-*}
-
 section {* Infrastructure for collecting theorems for starting the lifting *}
 
 ML {*
@@ -402,9 +359,9 @@
 *}
 
 ML {*
-val mk_babs = Const (@{const_name "Babs"}, dummyT)
-val mk_ball = Const (@{const_name "Ball"}, dummyT)
-val mk_bex  = Const (@{const_name "Bex"}, dummyT)
+val mk_babs = Const (@{const_name Babs}, dummyT)
+val mk_ball = Const (@{const_name Ball}, dummyT)
+val mk_bex  = Const (@{const_name Bex}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
 *}
 

--- a/UnusedQuotMain.thy	Tue Dec 01 12:16:45 2009 +0100
+++ b/UnusedQuotMain.thy	Tue Dec 01 14:04:00 2009 +0100
@@ -3,6 +3,51 @@
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 
 
+section {*  Infrastructure about definitions *}
+
+(* Does the same as 'subst' in a given theorem *)
+ML {*
+fun eqsubst_thm ctxt thms thm =
+  let
+    val goalstate = Goal.init (Thm.cprop_of thm)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_thm"
+    | SOME th => cprem_of th 1
+    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+    val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
+    val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
+    val rt = Goal.prove_internal [] cgoal (fn _ => tac);
+  in
+    @{thm equal_elim_rule1} OF [rt, thm]
+  end
+*}
+
+(* expects atomized definitions *)
+ML {*
+fun add_lower_defs_aux lthy thm =
+  let
+    val e1 = @{thm fun_cong} OF [thm];
+    val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
+    val g = simp_ids f
+  in
+    (simp_ids thm) :: (add_lower_defs_aux lthy g)
+  end
+  handle _ => [simp_ids thm]
+*}
+
+ML {*
+fun add_lower_defs lthy def =
+  let
+    val def_pre_sym = symmetric def
+    val def_atom = atomize_thm def_pre_sym
+    val defs_all = add_lower_defs_aux lthy def_atom
+  in
+    map Thm.varifyT defs_all
+  end
+*}
+
+
+
 ML {*
 fun repeat_eqsubst_thm ctxt thms thm =
   repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)