src/Tools/induct.ML
changeset 43333 2bdec7f430d3
parent 43326 47cf4bc789aa
child 44241 7943b69f0188
     1.1 --- a/src/Tools/induct.ML	Thu Jun 09 22:25:25 2011 +0200
     1.2 +++ b/src/Tools/induct.ML	Thu Jun 09 23:12:02 2011 +0200
     1.3 @@ -588,9 +588,10 @@
     1.4          val concl = Logic.strip_assums_concl goal;
     1.5        in
     1.6          Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
     1.7 -        |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule')
     1.8 +        |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
     1.9        end
    1.10 -  end handle General.Subscript => Seq.empty;
    1.11 +  end
    1.12 +  handle General.Subscript => Seq.empty;
    1.13  
    1.14  end;
    1.15