src/Provers/induct_method.ML
changeset 19861 620d90091788
parent 19482 9f11af8f7ef9
child 19904 9956ecabd9af
     1.1 --- a/src/Provers/induct_method.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/Provers/induct_method.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -228,8 +228,8 @@
     1.4          val rule' = Thm.incr_indexes (maxidx + 1) rule;
     1.5          val concl = Logic.strip_assums_concl goal;
     1.6        in
     1.7 -        Unify.smash_unifiers (thy, Envir.empty (#maxidx (Thm.rep_thm rule')),
     1.8 -          [(Thm.concl_of rule', concl)])
     1.9 +        Unify.smash_unifiers thy [(Thm.concl_of rule', concl)]
    1.10 +          (Envir.empty (#maxidx (Thm.rep_thm rule')))
    1.11          |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
    1.12        end
    1.13    end handle Subscript => Seq.empty;