# HG changeset patch
# User wenzelm
# Date 1273405145 -7200
# Node ID 0c5a8df725def467a960684fdea4f58396b3a5e1
# Parent  17427cf6fe9506244670ea9dce796cf408a715ca
removed unused "option" variants of "same" operations;

diff -r 17427cf6fe95 -r 0c5a8df725de src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Sun May 09 13:18:13 2010 +0200
+++ b/src/Pure/term_subst.ML	Sun May 09 13:39:05 2010 +0200
@@ -9,16 +9,10 @@
   val map_atypsT_same: typ Same.operation -> typ Same.operation
   val map_types_same: typ Same.operation -> term Same.operation
   val map_aterms_same: term Same.operation -> term Same.operation
-  val map_atypsT_option: (typ -> typ option) -> typ -> typ option
-  val map_atyps_option: (typ -> typ option) -> term -> term option
-  val map_types_option: (typ -> typ option) -> term -> term option
-  val map_aterms_option: (term -> term option) -> term -> term option
   val generalizeT_same: string list -> int -> typ Same.operation
   val generalize_same: string list * string list -> int -> term Same.operation
   val generalize: string list * string list -> int -> term -> term
   val generalizeT: string list -> int -> typ -> typ
-  val generalize_option: string list * string list -> int -> term -> term option
-  val generalizeT_option: string list -> int -> typ -> typ option
   val instantiateT_maxidx: ((indexname * sort) * (typ * int)) list -> typ -> int -> typ * int
   val instantiate_maxidx:
     ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
@@ -64,11 +58,6 @@
       | term a = f a;
   in term end;
 
-val map_atypsT_option = Same.capture o map_atypsT_same o Same.function;
-val map_atyps_option = Same.capture o map_types_same o map_atypsT_same o Same.function;
-val map_types_option = Same.capture o map_types_same o Same.function;
-val map_aterms_option = Same.capture o map_aterms_same o Same.function;
-
 
 (* generalization of fixed variables *)
 
@@ -102,9 +91,6 @@
 fun generalize names i tm = Same.commit (generalize_same names i) tm;
 fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty;
 
-fun generalize_option names i tm = SOME (generalize_same names i tm) handle Same.SAME => NONE;
-fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle Same.SAME => NONE;
-
 
 (* instantiation of schematic variables (types before terms) -- recomputes maxidx *)