diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Jan 01 23:59:32 2010 +0100
@@ -39,7 +39,7 @@
 
 fun atomize_thm thm =
 let
-  val thm' = Thm.freezeT (forall_intr_vars thm) (* TODO: is this proper Isar-technology? *)
+  val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
   val thm'' = ObjectLogic.atomize (cprop_of thm')
 in
   @{thm equal_elim_rule1} OF [thm'', thm']
@@ -60,7 +60,7 @@
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
 (* FIXME / TODO: test whether DETERM makes any runtime-difference *)
-(* FIXME / TODO: reason: it might back-track over the two alternatives in FIRST' *)
+(* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *)
 fun quotient_tac ctxt = SOLVES'  
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
@@ -84,15 +84,15 @@
 fun get_match_inst thy pat trm =
 let
   val univ = Unify.matchers thy [(pat, trm)]
-  val SOME (env, _) = Seq.pull univ                              (* raises BIND, if no unifier *)
+  val SOME (env, _) = Seq.pull univ                   (* raises BIND, if no unifier *)
   val tenv = Vartab.dest (Envir.term_env env)
   val tyenv = Vartab.dest (Envir.type_env env)
 in
   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 end
 
-(* calculates the instantiations for te lemmas *)
-(* ball_reg_eqv_range and bex_reg_eqv_range    *)
+(* calculates the instantiations for the lemmas *)
+(* ball_reg_eqv_range and bex_reg_eqv_range     *)
 fun calculate_inst ctxt ball_bex_thm redex R1 R2 =
 let
   fun get_lhs thm = fst (Logic.dest_equals (Thm.concl_of thm))
@@ -106,11 +106,11 @@
   SOME thm''
 end
 handle _ => NONE      
-(* FIXME/TODO: !!!CLEVER CODE!!!                                 *)
-(* FIXME/TODO: What is the place where the exception is raised,  *)
-(* FIXME/TODO: and which exception is it?                        *)
-(* FIXME/TODO: Can one not find out from the types of R1 or R2,  *)
-(* FIXME/TODO: or from their form, when NONE should be returned? *)
+(* FIXME/TODO: !!!CLEVER CODE!!!                                       *)
+(* FIXME/TODO: What are the places where the exceptions are raised,    *)
+(* FIXME/TODO: and which exception is it?                              *)
+(* FIXME/TODO: Can one not find out from the types of R1, R2 and redex *)
+(* FIXME/TODO: when NONE should be returned?                           *)
 
 fun ball_bex_range_simproc ss redex =
 let
@@ -231,10 +231,9 @@
 
 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 
-
-(* We apply apply_rsp only in case if the type needs lifting.      *)
-(* This is the case if the type of the data in the Quot_True       *)
-(* assumption is different from the corresponding type in the goal *)
+(* We apply apply_rsp only in case if the type needs lifting.       *)
+(* This is the case if the type of the data in the Quot_True        *)
+(* assumption is different from the corresponding type in the goal. *)
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
   let
@@ -269,13 +268,13 @@
 in
   rtac thm THEN' quotient_tac ctxt
 end
-(* TODO: Are they raised by instantiate'? *)
-(* TODO: Again, can one specify more concretely when no_tac should be returned? *)
+(* TODO: Are they raised by instantiate'?              *)
+(* TODO: Again, can one specify more concretely        *)
+(* TODO: in terms of R when no_tac should be returned? *)
 handle THM _  => K no_tac  
      | TYPE _ => K no_tac    
      | TERM _ => K no_tac
 
-
 fun rep_abs_rsp_tac ctxt = 
   SUBGOAL (fn (goal, i) =>
     case (bare_concl goal) of 
@@ -564,16 +563,16 @@
 (* The General Shape of the Lifting Procedure *)
 (**********************************************)
 
-(* - A is the original raw theorem                       *)
-(* - B is the regularized theorem                        *)
-(* - C is the rep/abs injected version of B              *)
-(* - D is the lifted theorem                             *)
-(*                                                       *)
-(* - 1st prem is the regularization step                 *)
-(* - 2nd prem is the rep/abs injection step              *)
-(* - 3rd prem is the cleaning part                       *)
-(*                                                       *)
-(* the Quot_True premise in 2 records the lifted theorem *)
+(* - A is the original raw theorem                         *)
+(* - B is the regularized theorem                          *)
+(* - C is the rep/abs injected version of B                *)
+(* - D is the lifted theorem                               *)
+(*                                                         *)
+(* - 1st prem is the regularization step                   *)
+(* - 2nd prem is the rep/abs injection step                *)
+(* - 3rd prem is the cleaning part                         *)
+(*                                                         *)
+(* the Quot_True premise in 2nd records the lifted theorem *)
 
 val lifting_procedure_thm = 
    @{lemma  "[|A;