changeset 26653 | 60e0cf6bef89 |
parent 26529 | 03ad378ed5f0 |
child 28083 | 103d9282a946 |
--- a/src/HOL/Tools/function_package/mutual.ML Tue Apr 15 16:12:01 2008 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Tue Apr 15 16:12:05 2008 +0200 @@ -222,7 +222,7 @@ fold (fn x => fn thm => combination thm (reflexive x)) xs thm |> Conv.fconv_rule (Thm.beta_conversion true) |> fold_rev forall_intr xs - |> forall_elim_vars 0 + |> Thm.forall_elim_vars 0 end