# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259689732 -3600
# Node ID cb03d4b3f059ee0220a931cc2beaee2bee43cc69
# Parent  8f9b74f921badcb265f0de68ea58a35e58fa80d2
fixed problems with FOCUS

diff -r 8f9b74f921ba -r cb03d4b3f059 QuotMain.thy
--- a/QuotMain.thy	Tue Dec 01 18:41:01 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 18:48:52 2009 +0100
@@ -770,11 +770,6 @@
 
 section {* RepAbs Injection Tactic *}
 
-ML {*
-fun stripped_term_of ct =
-  ct |> term_of |> HOLogic.dest_Trueprop
-*}
-
 (* TODO: check if it still works with first_order_match *)
 ML {*
 fun instantiate_tac thm = 
@@ -806,16 +801,16 @@
 
 ML {*
 val lambda_res_tac =
-  Subgoal.FOCUS (fn {concl, ...} =>
-    case (stripped_term_of concl) of
-       (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1
+  SUBGOAL (fn (goal, i) =>
+    case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
+       (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i
      | _ => no_tac)
 *}
 
 ML {*
 val weak_lambda_res_tac =
-  Subgoal.FOCUS (fn {concl, ...} =>
-    case (stripped_term_of concl) of
+  SUBGOAL (fn (goal, i) =>
+    case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
        (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1
      | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1
      | _ => no_tac)
@@ -823,8 +818,8 @@
 
 ML {*
 val ball_rsp_tac = 
-  Subgoal.FOCUS (fn {concl, ...} =>
-     case (stripped_term_of concl) of
+  SUBGOAL (fn (goal, i) =>
+    case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
         (_ $ (Const (@{const_name Ball}, _) $ _) 
            $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1
       |_ => no_tac)
@@ -832,8 +827,8 @@
 
 ML {*
 val bex_rsp_tac = 
-  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-     case (stripped_term_of concl) of
+  SUBGOAL (fn (goal, i) =>
+    case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
         (_ $ (Const (@{const_name Bex}, _) $ _) 
            $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1
       | _ => no_tac)
@@ -847,10 +842,13 @@
 
 *}
 
+
+
+
 ML {*
 fun APPLY_RSP_TAC rty = 
   Subgoal.FOCUS (fn {concl, ...} =>
-    case (stripped_term_of concl) of
+    case HOLogic.dest_Trueprop (term_of concl) of
        (_ $ (f $ _) $ (_ $ _)) =>
           let
             val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});