src/HOL/Tools/Function/induction_schema.ML
changeset 52467 24c6ddb48cb8
parent 52223 5bb6ae8acb87
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Thu Jun 27 12:34:58 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Thu Jun 27 17:06:22 2013 +0200
     1.3 @@ -328,7 +328,7 @@
     1.4        |> split_list |> apsnd flat
     1.5  
     1.6      val istep = sum_split_rule
     1.7 -      |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches
     1.8 +      |> fold (fn b => fn th => Drule.compose (b, 1, th)) branches
     1.9        |> Thm.implies_intr ihyp
    1.10        |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *)
    1.11