src/HOL/Tools/Function/induction_schema.ML
changeset 52223 5bb6ae8acb87
parent 51717 9e7d1c139569
child 52467 24c6ddb48cb8
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
   383       |> Drule.generalize ([], [Rn])
   383       |> Drule.generalize ([], [Rn])
   384 
   384 
   385     val nbranches = length branches
   385     val nbranches = length branches
   386     val npres = length pres
   386     val npres = length pres
   387   in
   387   in
   388     Thm.compose_no_flatten false (res, length newgoals) i
   388     Thm.bicompose {flatten = false, match = false, incremented = false}
       
   389       (false, res, length newgoals) i
   389     THEN term_tac (i + nbranches + npres)
   390     THEN term_tac (i + nbranches + npres)
   390     THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
   391     THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
   391     THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
   392     THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
   392   end))
   393   end))
   393 
   394