diff -r ee276c9f12f0 -r c7069b09730b Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Wed Feb 10 10:36:47 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Feb 10 10:55:14 2010 +0100
@@ -39,7 +39,7 @@
 
 (* prints a warning, if the subgoal is not solved *)
 fun WARN (tac, msg) i st =
- case Seq.pull ((SOLVED' tac) i st) of
+ case Seq.pull (SOLVED' tac i st) of
      NONE    => (warning msg; Seq.single st)
    | seqcell => Seq.make (fn () => seqcell)
 
@@ -178,7 +178,7 @@
 
 (*** Injection Tactic ***)
 
-(* Looks for Quot_True assumtions, and in case its parameter
+(* Looks for Quot_True assumptions, and in case its parameter
    is an application, it returns the function and the argument. 
 *)
 fun find_qt_asm asms =
@@ -442,12 +442,12 @@
 
 (* custom matching functions *)
 fun mk_abs u i t =
-  if incr_boundvars i u aconv t then Bound i
-  else (case t of
-     t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2)
-   | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
-   | Bound j => if i = j then error "make_inst" else t
-   | _ => t)
+  if incr_boundvars i u aconv t then Bound i else
+  case t of
+    t1 $ t2 => mk_abs u i t1 $ mk_abs u i t2
+  | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
+  | Bound j => if i = j then error "make_inst" else t
+  | _ => t
 
 fun make_inst lhs t =
 let
@@ -586,11 +586,11 @@
               C = D|] ==> D"
       by (simp add: Quot_True_def)}
 
-fun lift_match_error ctxt str rtrm qtrm =
+fun lift_match_error ctxt msg rtrm qtrm =
 let
   val rtrm_str = Syntax.string_of_term ctxt rtrm
   val qtrm_str = Syntax.string_of_term ctxt qtrm
-  val msg = cat_lines [enclose "[" "]" str, "The quotient theorem", qtrm_str, 
+  val msg = cat_lines [enclose "[" "]" msg, "The quotient theorem", qtrm_str, 
     "", "does not match with original theorem", rtrm_str]
 in
   error msg
@@ -602,9 +602,9 @@
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
-    handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
+    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
   val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
-    handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
+    handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),