--- a/src/Pure/proofterm.ML Fri Dec 15 17:15:59 2023 +0100
+++ b/src/Pure/proofterm.ML Fri Dec 15 17:19:57 2023 +0100
@@ -2253,7 +2253,7 @@
proof_combP (proof_combt' (head, args),
map PClass (#outer_constraints ucontext) @ map Hyp hyps);
val (zboxes2, zproof2) =
- if unconstrain then (ZTerm.empty_zboxes, ZTerm.todo_proof ())
+ if unconstrain then (#zboxes body1, #zproof body1) (* FIXME proper zproof *)
else (#zboxes body1, #zproof body1);
val proof_body =
--- a/src/Pure/zterm.ML Fri Dec 15 17:15:59 2023 +0100
+++ b/src/Pure/zterm.ML Fri Dec 15 17:19:57 2023 +0100
@@ -247,8 +247,6 @@
val norm_type: Type.tyenv -> ztyp -> ztyp
val norm_term: theory -> Envir.env -> zterm -> zterm
val norm_proof: theory -> Envir.env -> zproof -> zproof
- val dummy_proof: 'a -> zproof
- val todo_proof: 'a -> zproof
type zboxes = (zterm * zproof future) Inttab.table
val empty_zboxes: zboxes
val union_zboxes: zboxes -> zboxes -> zboxes
@@ -589,10 +587,6 @@
(** proof construction **)
-fun dummy_proof _ = ZDummy;
-val todo_proof = dummy_proof;
-
-
(* constants *)
type zproof_const = zproof_name * zterm * ztyp ZTVars.table * zterm ZVars.table;