# HG changeset patch
# User wenzelm
# Date 1695670606 -7200
# Node ID c2c4d51b048bfd6f2c36586f5f4c264f2b22387c
# Parent  3a3a70d4d422c8117c486e45853dbe19ac3adab9
unused;

diff -r 3a3a70d4d422 -r c2c4d51b048b src/Pure/General/same.ML
--- a/src/Pure/General/same.ML	Mon Sep 25 21:30:46 2023 +0200
+++ b/src/Pure/General/same.ML	Mon Sep 25 21:36:46 2023 +0200
@@ -13,7 +13,6 @@
   val same: ('a, 'b) function
   val commit: 'a operation -> 'a -> 'a
   val function: ('a -> 'b option) -> ('a, 'b) function
-  val capture: ('a, 'b) function -> 'a -> 'b option
   val map: 'a operation -> 'a list operation
   val map_option: ('a, 'b) function -> ('a option, 'b option) function
 end;
@@ -29,8 +28,6 @@
 fun same _ = raise SAME;
 fun commit f x = f x handle SAME => x;
 
-fun capture f x = SOME (f x) handle SAME => NONE;
-
 fun function f x =
   (case f x of
     NONE => raise SAME