changeset 54883 | dd04a8b654fc |
parent 54742 | 7a86358a3c0b |
child 57959 | 1bfed12a7646 |
--- a/src/HOL/Tools/Function/partial_function.ML Tue Dec 31 11:19:14 2013 +0100 +++ b/src/HOL/Tools/Function/partial_function.ML Tue Dec 31 14:29:16 2013 +0100 @@ -265,7 +265,7 @@ |> HOLogic.mk_Trueprop |> Logic.all x_uc; - val mono_thm = Goal.prove_internal [] (cert mono_goal) + val mono_thm = Goal.prove_internal lthy [] (cert mono_goal) (K (mono_tac lthy 1)) val inst_mono_thm = Thm.forall_elim (cert x_uc) mono_thm