# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260417228 -3600
# Node ID fa0f6fdac5de4fd68ff8cb8ccb6f31305d3fe83e
# Parent  cf1ad0e59d970e88c56647d64bbeb2e2142e9954
simplified the instantiation of QUOT_TRUE in procedure_tac

diff -r cf1ad0e59d97 -r fa0f6fdac5de Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 04:35:08 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 04:53:48 2009 +0100
@@ -1058,11 +1058,11 @@
 lemma lifting_procedure:
   assumes a: "A"
   and     b: "A \<longrightarrow> B"
-  and     c: "B = C"
+  and     c: "QUOT_TRUE D \<Longrightarrow> B = C"
   and     d: "C = D"
   shows   "D"
 using a b c d
-by simp
+by (simp add: QUOT_TRUE_def)
 
 ML {*
 fun lift_match_error ctxt fun_str rtrm qtrm =
@@ -1092,6 +1092,7 @@
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),
      SOME (cterm_of thy reg_goal),
+     NONE,
      SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
 end
 *}
@@ -1105,10 +1106,8 @@
     let
       val rthm' = atomize_thm rthm
       val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
-      val bare_goal = snd (Thm.dest_comb goal)
-      val quot_weak = Drule.instantiate' [] [SOME bare_goal] @{thm QUOT_TRUE_i}
     in
-      (rtac rule THEN' RANGE [rtac rthm', K all_tac, rtac quot_weak]) i
+      (rtac rule THEN' rtac rthm') i
     end)
 *}
 
@@ -1127,9 +1126,10 @@
 ML {*
 fun lift_tac ctxt rthm =
   procedure_tac ctxt rthm
-  THEN' RANGE_WARN [(regularize_tac ctxt,     "Regularize proof failed."),
-                    (all_inj_repabs_tac ctxt, "Injection proof failed."),
-                    (clean_tac ctxt,          "Cleaning proof failed.")]
+  THEN' RANGE_WARN 
+     [(regularize_tac ctxt,     "Regularize proof failed."),
+      (all_inj_repabs_tac ctxt, "Injection proof failed."),
+      (clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 
 section {* methods / interface *}