src/HOL/Tools/function_package/fundef_package.ML
changeset 21359 072e83a0b5bb
parent 21319 cf814e36f788
child 21391 a8809f46bd7f
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 14 15:29:50 2006 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Nov 14 15:29:52 2006 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4        val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
     1.5      in
     1.6        (name, lthy
     1.7 -         |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
     1.8 +         |> Proof.theorem_i PureThy.internalK NONE afterqed [[(goal, [])]]
     1.9           |> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
    1.10      end
    1.11  
    1.12 @@ -163,8 +163,7 @@
    1.13                                          [ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
    1.14          |> set_termination_rule termination
    1.15          |> Proof.theorem_i PureThy.internalK NONE
    1.16 -                           (total_termination_afterqed name data) NONE ("", [])
    1.17 -                           [(("", []), [(goal, [])])]
    1.18 +                           (total_termination_afterqed name data) [[(goal, [])]]
    1.19      end
    1.20  
    1.21