simplified/unified fundamental operations on types/terms/proofterms -- prefer Same.operation over "option" variant;

--- a/src/Pure/Proof/extraction.ML	Tue May 04 11:02:50 2010 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue May 04 12:30:15 2010 +0200
@@ -136,8 +136,7 @@
   | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
   | strip_abs _ _ = error "strip_abs: not an abstraction";
 
-fun prf_subst_TVars tye =
-  map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
+val prf_subst_TVars = map_proof_types o typ_subst_TVars;
 
 fun relevant_vars types prop = List.foldr (fn
       (Var ((a, _), T), vs) => (case strip_type T of

--- a/src/Pure/Proof/reconstruct.ML	Tue May 04 11:02:50 2010 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Tue May 04 12:30:15 2010 +0200
@@ -376,8 +376,7 @@
             val varify = map_type_tfree (fn p as (a, S) =>
               if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
           in
-            (maxidx', prfs', map_proof_terms (subst_TVars tye o
-               map_types varify) (typ_subst_TVars tye o varify) prf)
+            (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf)
           end
       | expand maxidx prfs prf = (maxidx, prfs, prf);
 

--- a/src/Pure/proofterm.ML	Tue May 04 11:02:50 2010 +0200
+++ b/src/Pure/proofterm.ML	Tue May 04 12:30:15 2010 +0200
@@ -58,8 +58,10 @@
   val strip_combt: proof -> proof * term option list
   val strip_combP: proof -> proof * proof list
   val strip_thm: proof_body -> proof_body
-  val map_proof_terms_option: (term -> term option) -> (typ -> typ option) -> proof -> proof
+  val map_proof_terms_same: term Same.operation -> typ Same.operation -> proof Same.operation
+  val map_proof_types_same: typ Same.operation -> proof Same.operation
   val map_proof_terms: (term -> term) -> (typ -> typ) -> proof -> proof
+  val map_proof_types: (typ -> typ) -> proof -> proof
   val fold_proof_terms: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
   val maxidx_proof: proof -> int -> int
   val size_of_proof: proof -> int
@@ -273,10 +275,8 @@
 val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
 fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
 
-fun map_proof_terms_option f g =
+fun map_proof_same term typ ofclass =
   let
-    val term = Same.function f;
-    val typ = Same.function g;
     val typs = Same.map typ;
 
     fun proof (Abst (s, T, prf)) =
@@ -292,22 +292,23 @@
           (proof prf1 %% Same.commit proof prf2
             handle Same.SAME => prf1 %% proof prf2)
       | proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
-      | proof (OfClass (T, c)) = OfClass (typ T, c)
+      | proof (OfClass T_c) = ofclass T_c
       | proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
       | proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts)
       | proof (PThm (i, ((a, prop, SOME Ts), body))) =
           PThm (i, ((a, prop, SOME (typs Ts)), body))
       | proof _ = raise Same.SAME;
-  in Same.commit proof end;
+  in proof end;
+
+fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c));
+fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ;
 
 fun same eq f x =
   let val x' = f x
   in if eq (x, x') then raise Same.SAME else x' end;
 
-fun map_proof_terms f g =
-  map_proof_terms_option
-   (fn t => SOME (same (op =) f t) handle Same.SAME => NONE)
-   (fn T => SOME (same (op =) g T) handle Same.SAME => NONE);
+fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g));
+fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f));
 
 fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
   | fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
@@ -696,17 +697,17 @@
 (***** generalization *****)
 
 fun generalize (tfrees, frees) idx =
-  map_proof_terms_option
-    (Term_Subst.generalize_option (tfrees, frees) idx)
-    (Term_Subst.generalizeT_option tfrees idx);
+  Same.commit (map_proof_terms_same
+    (Term_Subst.generalize_same (tfrees, frees) idx)
+    (Term_Subst.generalizeT_same tfrees idx));
 
 
 (***** instantiation *****)
 
 fun instantiate (instT, inst) =
-  map_proof_terms_option
-    (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
-    (Term_Subst.instantiateT_option instT);
+  Same.commit (map_proof_terms_same
+    (Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst))
+    (Term_Subst.instantiateT_same instT));
 
 
 (***** lifting *****)
@@ -757,9 +758,8 @@
   end;
 
 fun incr_indexes i =
-  map_proof_terms_option
-    (Same.capture (Logic.incr_indexes_same ([], i)))
-    (Same.capture (Logic.incr_tvar_same i));
+  Same.commit (map_proof_terms_same
+    (Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i));
 
 
 (***** proof by assumption *****)

--- a/src/Pure/term_subst.ML	Tue May 04 11:02:50 2010 +0200
+++ b/src/Pure/term_subst.ML	Tue May 04 12:30:15 2010 +0200
@@ -13,6 +13,8 @@
   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
@@ -21,12 +23,12 @@
   val instantiate_maxidx:
     ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
     term -> int -> term * int
+  val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
   val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
     term -> term
-  val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
-  val instantiate_option: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
-    term -> term option
-  val instantiateT_option: ((indexname * sort) * typ) list -> typ -> typ option
+  val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
+  val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
+    term Same.operation
   val zero_var_indexes: term -> term
   val zero_var_indexes_inst: term list ->
     ((indexname * sort) * typ) list * ((indexname * typ) * term) list
@@ -70,8 +72,6 @@
 
 (* generalization of fixed variables *)
 
-local
-
 fun generalizeT_same [] _ _ = raise Same.SAME
   | generalizeT_same tfrees idx ty =
       let
@@ -99,16 +99,12 @@
           | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u);
       in gen tm end;
 
-in
-
-fun generalize names i tm = generalize_same names i tm handle Same.SAME => tm;
-fun generalizeT names i ty = generalizeT_same names i ty handle Same.SAME => ty;
+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;
 
-end;
-
 
 (* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
 
@@ -118,7 +114,7 @@
 fun no_indexes1 inst = map no_index inst;
 fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
 
-fun instantiateT_same maxidx instT ty =
+fun instT_same maxidx instT ty =
   let
     fun maxify i = if i > ! maxidx then maxidx := i else ();
 
@@ -134,11 +130,11 @@
       | subst_typs [] = raise Same.SAME;
   in subst_typ ty end;
 
-fun instantiate_same maxidx (instT, inst) tm =
+fun inst_same maxidx (instT, inst) tm =
   let
     fun maxify i = if i > ! maxidx then maxidx := i else ();
 
-    val substT = instantiateT_same maxidx instT;
+    val substT = instT_same maxidx instT;
     fun subst (Const (c, T)) = Const (c, substT T)
       | subst (Free (x, T)) = Free (x, substT T)
       | subst (Var ((x, i), T)) =
@@ -158,31 +154,23 @@
 
 fun instantiateT_maxidx instT ty i =
   let val maxidx = Unsynchronized.ref i
-  in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
+  in (Same.commit (instT_same maxidx instT) ty, ! maxidx) end;
 
 fun instantiate_maxidx insts tm i =
   let val maxidx = Unsynchronized.ref i
-  in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
+  in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
 
 fun instantiateT [] ty = ty
-  | instantiateT instT ty =
-      (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
-        handle Same.SAME => ty);
+  | instantiateT instT ty = Same.commit (instT_same (Unsynchronized.ref ~1) (no_indexes1 instT)) ty;
 
 fun instantiate ([], []) tm = tm
-  | instantiate insts tm =
-      (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
-        handle Same.SAME => tm);
+  | instantiate insts tm = Same.commit (inst_same (Unsynchronized.ref ~1) (no_indexes2 insts)) tm;
 
-fun instantiateT_option [] _ = NONE
-  | instantiateT_option instT ty =
-      (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
-        handle Same.SAME => NONE);
+fun instantiateT_same [] _ = raise Same.SAME
+  | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty;
 
-fun instantiate_option ([], []) _ = NONE
-  | instantiate_option insts tm =
-      (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
-        handle Same.SAME => NONE);
+fun instantiate_same ([], []) _ = raise Same.SAME
+  | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm;
 
 end;
 

--- a/src/Pure/variable.ML	Tue May 04 11:02:50 2010 +0200
+++ b/src/Pure/variable.ML	Tue May 04 12:30:15 2010 +0200
@@ -376,9 +376,9 @@
     val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
     val tfrees = mk_tfrees [];
     val idx = Proofterm.maxidx_proof prf ~1 + 1;
-    val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
-    val gen_typ = Term_Subst.generalizeT_option tfrees idx;
-  in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
+    val gen_term = Term_Subst.generalize_same (tfrees, frees) idx;
+    val gen_typ = Term_Subst.generalizeT_same tfrees idx;
+  in Same.commit (Proofterm.map_proof_terms_same gen_term gen_typ) prf end;
 
 
 fun gen_export (mk_tfrees, frees) ths =