--- a/Quot/quotient_tacs.ML	Wed Dec 23 23:22:02 2009 +0100
+++ b/Quot/quotient_tacs.ML	Wed Dec 23 23:53:03 2009 +0100
@@ -23,13 +23,13 @@
 
 (* various helper fuctions *)
 
-(* composition of two theorems, used in map *)
+(* composition of two theorems, used in maps *)
 fun OF1 thm1 thm2 = thm2 RS thm1
 
 (* makes sure a subgoal is solved *)
 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
 
-(* prints warning, if goal is unsolved *)
+(* prints warning, if the subgoal is unsolved *)
 fun WARN (tac, msg) i st =
  case Seq.pull ((SOLVES' tac) i st) of
      NONE    => (warning msg; Seq.single st)
@@ -426,6 +426,7 @@
 
 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
 
+
 fun mk_abs u i t =
   if incr_boundvars i u aconv t then Bound i
   else (case t of
@@ -454,7 +455,7 @@
 (* First instantiates the types and known subterms.          *)
 (* Then solves the quotient assumptions to get Rep2 and Abs1 *)
 (* Finally instantiates the function f using make_inst       *)
-(* If Rep2 is identity then the pattern is simpler and       *)
+(* If Rep2 is an identity then the pattern is simpler and    *)
 (* make_inst_id is used                                      *)
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
@@ -468,8 +469,10 @@
        val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
        val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
        val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
-       val make_inst = if ty_c = ty_d then make_inst_id else make_inst
-       val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
+       val (insp, inst) = 
+              if ty_c = ty_d 
+              then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)
+              else make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
      in
        Conv.rewr_conv ti ctrm
@@ -500,28 +503,28 @@
 (* 5. test for refl                                    *)
 
 fun clean_tac_aux lthy =
-  let
-    val thy = ProofContext.theory_of lthy;
-    val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+let
+  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
-  in
-    EVERY' [simp_tac (simps thms1),
-            fun_map_tac lthy,
-            lambda_prs_tac lthy,
-            simp_tac (simps thms2),
-            TRY o rtac refl]
-  end
+  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
+in
+  EVERY' [simp_tac (simps thms1),
+          fun_map_tac lthy,
+          lambda_prs_tac lthy,
+          simp_tac (simps thms2),
+          TRY o rtac refl]  
+end
 
 fun clean_tac lthy = REPEAT o CHANGED o (clean_tac_aux lthy) (* HACK?? *)
 
 
-(********************************************************)
-(* Tactic for Genralisation of Free Variables in a Goal *)
-(********************************************************)
+(****************************************************)
+(* Tactic for Generalising Free Variables in a Goal *)
+(****************************************************)
 
 fun inst_spec ctrm =
    Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}
@@ -603,10 +606,10 @@
 fun procedure_tac ctxt rthm =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac ctxt
-  THEN' CSUBGOAL (fn (goal, i) =>
+  THEN' SUBGOAL (fn (goal, i) =>
     let
       val rthm' = atomize_thm rthm
-      val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
+      val rule = procedure_inst ctxt (prop_of rthm') goal
     in
       (rtac rule THEN' rtac rthm') i
     end)

--- a/Quot/quotient_term.ML	Wed Dec 23 23:22:02 2009 +0100
+++ b/Quot/quotient_term.ML	Wed Dec 23 23:53:03 2009 +0100
@@ -145,7 +145,7 @@
        if s = s' 
        then 
          let
-           val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s ^ ")") 
+           val exc = LIFT_MATCH ("mk_resp_arg (no relation map function found for type " ^ s ^ ")") 
            val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exc
            val args = map (mk_resp_arg ctxt) (tys ~~ tys')
          in
@@ -188,7 +188,7 @@
 
 (* produces a regularized version of rtrm       *)
 (*                                              *)
-(* - the result still contains dummyTs          *)
+(* - the result might contain dummyTs           *)
 (*                                              *)
 (* - for regularisation we do not need any      *)
 (*   special treatment of bound variables       *)
@@ -228,7 +228,7 @@
     (rel, Const (@{const_name "op ="}, ty')) =>
        let 
          val exc = LIFT_MATCH "regularise (relation mismatch)"
-         val rel_ty = (fastype_of rel) handle TERM _ => raise exc 
+         val rel_ty = fastype_of rel
          val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty') 
        in 
          if rel' aconv rel then rtrm else raise exc
@@ -258,7 +258,7 @@
              val qtrm_str = Syntax.string_of_term ctxt qtrm
              val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
              val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
-             val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
+             val rtrm' = #rconst (qconsts_lookup thy qtrm) handle NotFound => raise exc1
            in 
              if Pattern.matches thy (rtrm', rtrm) 
              then rtrm else raise exc2