src/HOL/Tools/function_package/fundef_package.ML
changeset 22325 be61bd159a99
parent 22170 5682eeaefaf4
child 22498 62cdd4b3e96b
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Feb 15 12:14:34 2007 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Feb 15 17:35:19 2007 +0100
     1.3 @@ -166,11 +166,14 @@
     1.4                     handle Option.Option => raise ERROR ("No such function definition: " ^ defname)
     1.5  
     1.6          val FundefCtxData {termination, R, ...} = data
     1.7 -        val goal = FundefTermination.mk_total_termination_goal R
     1.8 +        val domT = domain_type (fastype_of R)
     1.9 +        val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
    1.10      in
    1.11        lthy
    1.12 +        |> ProofContext.note_thmss_i "" [(("", [ContextRules.rule_del]), [([allI], [])])] |> snd
    1.13 +        |> ProofContext.note_thmss_i "" [(("", [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
    1.14          |> ProofContext.note_thmss_i ""
    1.15 -          [(("termination", [ContextRules.intro_query NONE]),
    1.16 +          [(("termination", [ContextRules.intro_bang (SOME 0)]),
    1.17              [([Goal.norm_result termination], [])])] |> snd
    1.18          |> set_termination_rule termination
    1.19          |> Proof.theorem_i NONE (total_termination_afterqed defname data) [[(goal, [])]]