--- a/QuotMain.thy	Tue Nov 24 19:09:29 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 03:45:44 2009 +0100
@@ -1172,16 +1172,6 @@
 val mk_resp = Const (@{const_name Respects}, dummyT)
 *}
 
-ML {*
-fun trm_lift_error lthy rtrm qtrm =
-let
-  val rtrm_str = quote (Syntax.string_of_term lthy rtrm) 
-  val qtrm_str = quote (Syntax.string_of_term lthy qtrm)
-  val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]
-in
-  raise error (space_implode " " msg)
-end 
-*}
 
 ML {*
 (* - applies f to the subterm of an abstraction,   *)
@@ -1265,16 +1255,23 @@
   | (Free (x, ty), Free (x', ty')) =>
        if x = x' 
        then rtrm     (* FIXME: check whether types corresponds *)
-       else trm_lift_error lthy rtrm qtrm
+       else raise (LIFT_MATCH "regularize (frees)")
   | (Bound i, Bound i') =>
        if i = i' 
        then rtrm 
-       else trm_lift_error lthy rtrm qtrm
+       else raise (LIFT_MATCH "regularize (bounds)")
   | (Const (s, ty), Const (s', ty')) =>
        if s = s' andalso ty = ty'
        then rtrm
        else rtrm (* FIXME: check correspondence according to definitions *) 
-  | _ => trm_lift_error lthy rtrm qtrm
+  | (rt, qt) => 
+     let
+       val _ = tracing "default execption"
+       val _ = tracing (PolyML.makestring rt)
+       val _ = tracing (PolyML.makestring qt)
+     in
+       raise (LIFT_MATCH "regularize (default)")
+     end
 *}
 
 ML {*
@@ -1433,7 +1430,7 @@
                mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
           | (Abs _, Abs _, _ ) =>
                mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) 
-          | _ => trm_lift_error lthy rtrm qtrm
+          | _ => raise (LIFT_MATCH "injection")
       end
 end
 *}
@@ -1528,22 +1525,33 @@
 *}
 
 ML {*
-fun spec_frees_tac [] = []
-  | spec_frees_tac (x::xs) = 
-       let
-         val spec' =  Drule.instantiate' [SOME (ctyp_of_term x)] [NONE, SOME x] @{thm spec} 
-       in
-         (rtac spec')::(spec_frees_tac xs)
-       end
-*}  
+fun inst_spec ctrm =
+let
+   val cty = ctyp_of_term ctrm
+in
+   Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
+end
+
+fun inst_spec_tac ctrms =
+  EVERY' (map (dtac o inst_spec) ctrms)
+
+fun abs_list (xs, t) = 
+  fold (fn (x, T) => fn t' => HOLogic.all_const T $ (lambda (Free (x, T)) t')) xs t
 
-ML {*
-val prepare_tac = CSUBGOAL (fn (concl, i) =>
-    let
-      val vrs = Thm.add_cterm_frees concl []
-    in
-      EVERY' (ObjectLogic.full_atomize_tac::spec_frees_tac vrs) i
-    end)
+fun gen_frees_tac ctxt =
+ SUBGOAL (fn (concl, i) =>
+  let
+    val thy = ProofContext.theory_of ctxt
+    val concl' = HOLogic.dest_Trueprop concl
+    val vrs = Term.add_frees concl' []
+    val cvrs = map (cterm_of thy o Free) vrs
+    val concl'' = HOLogic.mk_Trueprop (abs_list (vrs, concl'))
+    val goal = Logic.mk_implies (concl'', concl)
+    val rule = Goal.prove ctxt [] [] goal 
+      (K ((inst_spec_tac (rev cvrs) THEN' atac) 1))
+  in
+    rtac rule i
+  end)  
 *}
 
 lemma procedure:
@@ -1555,6 +1563,18 @@
   using a b c d
   by simp
 
+ML {*
+fun lift_error ctxt fun_str rtrm qtrm =
+let
+  val rtrm_str = Syntax.string_of_term ctxt rtrm
+  val qtrm_str = Syntax.string_of_term ctxt qtrm
+  val msg = [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, 
+             "and the lifted theorem", rtrm_str, "do not match"]
+in
+  error (space_implode " " msg)
+end
+*}
+
 ML {* 
 fun procedure_inst ctxt rtrm qtrm =
 let
@@ -1562,7 +1582,9 @@
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
+                 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
   val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
+                 handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
 in
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),
@@ -1574,17 +1596,19 @@
   
 ML {*
 fun procedure_tac rthm ctxt =
-  prepare_tac THEN'
-  Subgoal.FOCUS (fn {context, concl, ...} =>
-    let
-      val rthm' = atomize_thm rthm
-      val rule = procedure_inst context (prop_of rthm') (term_of concl)
-    in
-      EVERY1 [rtac rule, rtac rthm']
-    end) ctxt
+  ObjectLogic.full_atomize_tac 
+  THEN' gen_frees_tac ctxt
+  THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
+          let
+            val rthm' = atomize_thm rthm
+            val rule = procedure_inst context (prop_of rthm') (Envir.beta_norm (term_of concl))
+          in
+           EVERY1 [rtac rule, rtac rthm']
+        end) ctxt
 *}
 
 
+
 ML {*
 (* FIXME: allex_prs and lambda_prs can be one function *)
 fun allex_prs_tac lthy quot =
@@ -1618,7 +1642,7 @@
   val univ = Unify.matchers thy [(pat, trm)] 
   val SOME (env, _) = Seq.pull univ
   val tenv = Vartab.dest (Envir.term_env env)
-  val tyenv =  Vartab.dest (Envir.type_env env)
+  val tyenv = Vartab.dest (Envir.type_env env)
 in
   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 end