# HG changeset patch
# User wenzelm
# Date 1702657197 -3600
# Node ID 5f95ba88d686a585462ccb2432a71f387b14510e
# Parent  3c194f50beefa6235ebc18b6b15d8ef1cb1f4829
tuned signature;

diff -r 3c194f50beef -r 5f95ba88d686 src/Pure/proofterm.ML
--- 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 =
diff -r 3c194f50beef -r 5f95ba88d686 src/Pure/zterm.ML
--- 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;