# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259691523 -3600
# Node ID 1eeacabe5ffe6d640ef33c486df488b346cfe335
# Parent  5e1f4c8ab3de83c0a381d48d198dbda91b8165c8
back in working state

diff -r 5e1f4c8ab3de -r 1eeacabe5ffe FSet.thy
--- a/FSet.thy	Tue Dec 01 19:01:51 2009 +0100
+++ b/FSet.thy	Tue Dec 01 19:18:43 2009 +0100
@@ -304,7 +304,6 @@
 
 thm m1
 
-
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context}  [rel_eqv] 1 *})
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;