# HG changeset patch
# User wenzelm
# Date 1302978170 -7200
# Node ID bfd28ba57859f5c192615685e3f496ae861686e7
# Parent  8c674b3b8e4488501bf868da2165c1973ff47a36
more direct Logic.dest_implies (with exception TERM instead of Subscript);

diff -r 8c674b3b8e44 -r bfd28ba57859 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Sat Apr 16 18:11:20 2011 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Sat Apr 16 20:22:50 2011 +0200
@@ -148,7 +148,7 @@
             error "splitto: cannot find variable to split on")
         | SOME v =>
             let
-              val gt = HOLogic.dest_Trueprop (nth (Thm.prems_of th) 0);
+              val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
               val split_thm = mk_casesplit_goal_thm thy v gt;
               val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
             in