src/HOL/Tools/Function/induction_schema.ML
changeset 52223 5bb6ae8acb87
parent 51717 9e7d1c139569
child 52467 24c6ddb48cb8
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed May 29 16:12:05 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed May 29 18:25:11 2013 +0200
     1.3 @@ -385,7 +385,8 @@
     1.4      val nbranches = length branches
     1.5      val npres = length pres
     1.6    in
     1.7 -    Thm.compose_no_flatten false (res, length newgoals) i
     1.8 +    Thm.bicompose {flatten = false, match = false, incremented = false}
     1.9 +      (false, res, length newgoals) i
    1.10      THEN term_tac (i + nbranches + npres)
    1.11      THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
    1.12      THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))