diff -r 5e1f4c8ab3de -r 1eeacabe5ffe QuotMain.thy
--- a/QuotMain.thy	Tue Dec 01 19:01:51 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 19:18:43 2009 +0100
@@ -800,7 +800,7 @@
 ML {*
 val lambda_res_tac =
   SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
+    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
        (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i
      | _ => no_tac)
 *}
@@ -808,7 +808,7 @@
 ML {*
 val weak_lambda_res_tac =
   SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
+    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
        (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i
      | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i
      | _ => no_tac)
@@ -817,7 +817,7 @@
 ML {*
 val ball_rsp_tac = 
   SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
+    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
         (_ $ (Const (@{const_name Ball}, _) $ _) 
            $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i
       |_ => no_tac)
@@ -826,7 +826,7 @@
 ML {*
 val bex_rsp_tac = 
   SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
+    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
         (_ $ (Const (@{const_name Bex}, _) $ _) 
            $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i
       | _ => no_tac)
@@ -913,7 +913,7 @@
         (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
       | _ => false
   in
-    case find_first find_fun (Logic.strip_imp_prems gl) of
+    case find_first find_fun (Logic.strip_assums_hyp gl) of
       SOME (_ $ (_ $ x)) =>
         let
           val fx = fnctn x;