--- a/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 14 15:29:50 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Nov 14 15:29:52 2006 +0100
@@ -121,7 +121,7 @@
val afterqed = fundef_afterqed config fixes spec mutual_info name prep_result
in
(name, lthy
- |> Proof.theorem_i PureThy.internalK NONE afterqed NONE ("", []) [(("", []), [(goal, [])])]
+ |> Proof.theorem_i PureThy.internalK NONE afterqed [[(goal, [])]]
|> Proof.refine (Method.primitive_text (fn _ => goalI)) |> Seq.hd)
end
@@ -163,8 +163,7 @@
[ContextRules.intro_query NONE]), [(ProofContext.standard lthy [termination], [])])] |> snd
|> set_termination_rule termination
|> Proof.theorem_i PureThy.internalK NONE
- (total_termination_afterqed name data) NONE ("", [])
- [(("", []), [(goal, [])])]
+ (total_termination_afterqed name data) [[(goal, [])]]
end