Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more direct Logic.dest_implies (with exception TERM instead of Subscript);
authorwenzelm
Sat, 16 Apr 2011 20:22:50 +0200
changeset 42365 bfd28ba57859
parent 42364 8c674b3b8e44
child 42366 2305c70ec9b1
more direct Logic.dest_implies (with exception TERM instead of Subscript);
src/HOL/Tools/TFL/casesplit.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle