src/HOL/Tools/function_package/fundef_package.ML
changeset 24977 9f98751c9628
parent 24867 e5b55d7be9bb
child 25045 12386aefe9ac
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 11 19:10:17 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 11 19:10:19 2007 +0200
     1.3 @@ -202,7 +202,7 @@
     1.4  
     1.5        val t' = new_subg
     1.6                  |> fold forall_elim cps
     1.7 -                |> flip implies_elim (fold forall_elim cps sg2)
     1.8 +                |> Thm.elim_implies (fold forall_elim cps sg2)
     1.9                  |> fold_rev forall_intr cps
    1.10  
    1.11        val st' = implies_elim st t'