src/Pure/Isar/element.ML

--- a/src/Pure/Isar/element.ML	Sat Apr 15 23:11:08 2023 +0200
+++ b/src/Pure/Isar/element.ML	Mon Apr 17 23:32:46 2023 +0200
@@ -266,7 +266,7 @@
 
 val mark_witness = Logic.protect;
 fun witness_prop (Witness (t, _)) = t;
-fun witness_hyps (Witness (_, th)) = Termset.dest (Thm.hyps_of th);
+fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
 fun map_witness f (Witness witn) = Witness (f witn);
 
 fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));