Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/case_product.ML
changeset 67522 9e712280cc37
parent 67149 e61557884799 
--- a/src/Tools/case_product.ML	Sun Jan 28 16:09:00 2018 +0100
+++ b/src/Tools/case_product.ML	Sun Jan 28 19:28:52 2018 +0100
@@ -48,8 +48,8 @@
     val concl = Thm.concl_of thm1
 
     fun is_consumes t = not (Logic.strip_assums_concl t aconv concl)
-    val (p_cons1, p_cases1) = take_prefix is_consumes (Thm.prems_of thm1)
-    val (p_cons2, p_cases2) = take_prefix is_consumes (Thm.prems_of thm2)
+    val (p_cons1, p_cases1) = chop_prefix is_consumes (Thm.prems_of thm1)
+    val (p_cons2, p_cases2) = chop_prefix is_consumes (Thm.prems_of thm2)
 
     val p_cases_prod = map (fn p1 => map (fn p2 =>
       let
isabelle