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/HOL/Tools/Function/induction_schema.ML
changeset 52223 5bb6ae8acb87
parent 51717 9e7d1c139569
child 52467 24c6ddb48cb8 
--- a/src/HOL/Tools/Function/induction_schema.ML	Wed May 29 16:12:05 2013 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed May 29 18:25:11 2013 +0200
@@ -385,7 +385,8 @@
     val nbranches = length branches
     val npres = length pres
   in
-    Thm.compose_no_flatten false (res, length newgoals) i
+    Thm.bicompose {flatten = false, match = false, incremented = false}
+      (false, res, length newgoals) i
     THEN term_tac (i + nbranches + npres)
     THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
     THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
isabelle