# HG changeset patch
# User wenzelm
# Date 1158353773 -7200
# Node ID 8ef25fe585a88fb2a1b39ce2dc54891a49683698
# Parent  796ae7fa10496c958c2514cf06b0adb51cbd15b4
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);

diff -r 796ae7fa1049 -r 8ef25fe585a8 TFL/tfl.ML
--- a/TFL/tfl.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/TFL/tfl.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -389,8 +389,8 @@
                                              quote fid ^ " but found one of " ^
                                       quote x)
                     else x ^ "_def"
-     val wfrec_R_M =  map_term_types poly_tvars
-                          (wfrec $ map_term_types poly_tvars R)
+     val wfrec_R_M =  map_types poly_tvars
+                          (wfrec $ map_types poly_tvars R)
                       $ functional
      val def_term = mk_const_def (Theory.sign_of thy) (x, Ty, wfrec_R_M)
      val ([def], thy') = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -530,7 +530,7 @@
         (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map
            (fn (S, x) =>
               let
-                val S = map_term_types (map_type_tfree
+                val S = map_types (map_type_tfree
                   (fn (s, cs) => TFree (s, cs union cp_classes))) S;
                 val T = HOLogic.dest_setT (fastype_of S);
                 val permT = mk_permT (Type (name, []))
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -170,7 +170,7 @@
   (let
     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
     fun varify (t, (i, ts)) =
-      let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
+      let val t' = map_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
       in (maxidx_of_term t', t'::ts) end;
     val (i, cs') = foldr varify (~1, []) cs;
     val (i', intr_ts') = foldr varify (i, []) intr_ts;
@@ -180,7 +180,7 @@
       let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
     val (env, _) = fold unify rec_consts (Vartab.empty, i');
-    val subst = Type.freeze o map_term_types (Envir.norm_type env)
+    val subst = Type.freeze o map_types (Envir.norm_type env)
 
   in (map subst cs', map subst intr_ts')
   end) handle Type.TUNIFY =>
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -446,7 +446,7 @@
 				  SOME x => x
 				| NONE   => raise Type.TYPE_MATCH (* no match found - perhaps due to sort constraints *))
 		in
-			map_term_types
+			map_types
 				(map_type_tvar
 					(fn v =>
 						case Type.lookup (typeSubs, v) of
@@ -461,7 +461,7 @@
 		(* term 't'                                                            *)
 		(* (Term.sort * Term.typ) Term.Vartab.table -> Term.term -> Term.term *)
 		fun monomorphic_term typeSubs t =
-			map_term_types (map_type_tvar
+			map_types (map_type_tvar
 				(fn v =>
 					case Type.lookup (typeSubs, v) of
 					  NONE =>
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -108,7 +108,7 @@
                  NONE => TVar f
                | SOME (b, _) => TFree (b, S))
     in
-        map_term_types (map_type_tvar unthaw) t
+        map_types (map_type_tvar unthaw) t
     end
 
 (* The syntactic meddling needed to setup add_specification for work *)
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Provers/IsaPlanner/isand.ML
--- a/src/Provers/IsaPlanner/isand.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Provers/IsaPlanner/isand.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -173,7 +173,7 @@
     in trec ty end;
 
 (* implicit types and term *)
-fun allify_term_typs ty = Term.map_term_types (allify_typ ty);
+fun allify_term_typs ty = Term.map_types (allify_typ ty);
 
 (* allified version of term, given frees to allify over. Note that we
 only allify over the types on the given allified cterm, we can't do
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Provers/IsaPlanner/rw_tools.ML
--- a/src/Provers/IsaPlanner/rw_tools.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Provers/IsaPlanner/rw_tools.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -120,7 +120,7 @@
 (* map a function f to each type variable in a term *)
 (* implicit arg: term *)
 fun map_to_term_tvars f =
-    Term.map_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x);
+    Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x);   (* FIXME map_atyps !? *)
 
 
 
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Isar/element.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -381,7 +381,7 @@
 
 fun instT_term env =
   if Symtab.is_empty env then I
-  else Term.map_term_types (instT_type env);
+  else Term.map_types (instT_type env);
 
 fun instT_subst env th = (Drule.fold_terms o Term.fold_types o Term.fold_atyps)
   (fn T as TFree (a, _) =>
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -2119,7 +2119,7 @@
             TFree ((the o AList.lookup (op =) (new_Tnames ~~ new_Tnames')) a, s));
     val rename =
           if is_local then I
-          else Term.map_term_types renameT;
+          else Term.map_types renameT;
 
     val tinst = Symtab.make (map
                 (fn ((x, 0), T) => (x, T |> renameT)
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -97,7 +97,7 @@
     val instT2 = Envir.norm_type
       (#1 (fold (unify_vartypes thy vars1) internal_insts (Vartab.empty, 0)));
     val vars2 = map (apsnd instT2) vars1;
-    val internal_insts2 = map (apsnd (map_term_types instT2)) internal_insts;
+    val internal_insts2 = map (apsnd (map_types instT2)) internal_insts;
     val inst2 = instantiate internal_insts2;
 
 
@@ -110,7 +110,7 @@
 
     val instT3 = Term.typ_subst_TVars inferred;
     val vars3 = map (apsnd instT3) vars2;
-    val internal_insts3 = map (apsnd (map_term_types instT3)) internal_insts2;
+    val internal_insts3 = map (apsnd (map_types instT3)) internal_insts2;
     val external_insts3 = xs ~~ ts;
     val inst3 = instantiate external_insts3;
 
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Proof/extraction.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -277,7 +277,7 @@
   | freeze T = T;
 
 fun freeze_thaw f x =
-  map_term_types thaw (f (map_term_types freeze x));
+  map_types thaw (f (map_types freeze x));
 
 fun etype_of thy vs Ts t =
   let
@@ -324,7 +324,7 @@
       val T = etype_of thy' vs [] prop;
       val (T', thw) = Type.freeze_thaw_type
         (if T = nullT then nullT else map fastype_of vars' ---> T);
-      val t = map_term_types thw (term_of (read_cterm thy' (s1, T')));
+      val t = map_types thw (term_of (read_cterm thy' (s1, T')));
       val r' = freeze_thaw (condrew thy' eqns
         (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
           (Const ("realizes", T --> propT --> propT) $
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -128,7 +128,7 @@
     val thms = PureThy.all_thms_of thy;
     val axms = Theory.all_axioms_of thy;
 
-    fun mk_term t = (if ty then I else map_term_types (K dummyT))
+    fun mk_term t = (if ty then I else map_types (K dummyT))
       (Term.no_dummy_patterns t);
 
     fun prf_of [] (Bound i) = PBound i
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -379,7 +379,7 @@
               if p mem tfrees then TVar ((a, ~1), S) else TFree p)
           in
             (maxidx', prfs', map_proof_terms (subst_TVars tye o
-               map_term_types varify) (typ_subst_TVars tye o varify) prf)
+               map_types varify) (typ_subst_TVars tye o varify) prf)
           end
       | expand maxidx prfs prf = (maxidx, prfs, prf);
 
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -416,7 +416,7 @@
             val t' = case mk_typnorm thy_read (ty', ty)
              of NONE => error ("superfluous definition for constant " ^
                   quote c ^ "::" ^ Sign.string_of_typ thy_read ty)
-              | SOME norm => map_term_types norm t
+              | SOME norm => map_types norm t
           in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
       in fold_map read defs cs end;
     val (defs, _) = assume_arities_thy theory arities_pair (read_defs raw_defs cs);
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/axclass.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -285,7 +285,7 @@
             " needs to be weaker than " ^ Pretty.string_of_sort pp super)
       | [] => t
       | _ => error ("Multiple type variables in class axiom:\n" ^ Pretty.string_of_term pp t))
-      |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
+      |> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
       |> Logic.close_form;
 
     val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/codegen.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -1010,7 +1010,7 @@
       | strip t = t;
     val (gi, frees) = Logic.goal_params
       (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
-    val gi' = ObjectLogic.atomize_term thy (map_term_types
+    val gi' = ObjectLogic.atomize_term thy (map_types
       (map_type_tfree (fn p as (s, _) =>
         the_default (the_default (TFree p) default_type)
           (AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi)));
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/compress.ML
--- a/src/Pure/compress.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/compress.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -61,6 +61,6 @@
           (case Termtab.lookup (! terms) t of
             SOME t' => t'
           | NONE => (change terms (Termtab.update (t, t)); t));
-  in compress o map_term_types (typ thy) end;
+  in compress o map_types (typ thy) end;
 
 end;
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/consts.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -250,7 +250,7 @@
 fun abbreviate pp tsig naming mode ((c, raw_rhs), authentic) consts =
   let
     val rhs = raw_rhs
-      |> Term.map_term_types (Type.cert_typ tsig)
+      |> Term.map_types (Type.cert_typ tsig)
       |> certify pp tsig (consts |> expand_abbrevs false);
     val rhs' = rhs
       |> certify pp tsig (consts |> expand_abbrevs true);
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/envir.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -268,7 +268,7 @@
   in subst T end;
 
 (*Substitute for type Vars in a term*)
-val subst_TVars = map_term_types o typ_subst_TVars;
+val subst_TVars = map_types o typ_subst_TVars;
 
 (*Substitute for Vars in a term *)
 fun subst_Vars itms t = if Vartab.is_empty itms then t else
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/logic.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -555,7 +555,7 @@
     (fn Free (x, T) => Var ((x, 0), T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | t => t)
-  |> Term.map_term_types varifyT
+  |> Term.map_types varifyT
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 fun unvarify tm =
@@ -564,7 +564,7 @@
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | Free (x, _) => raise TERM (bad_fixed x, [tm])
       | t => t)
-  |> Term.map_term_types unvarifyT
+  |> Term.map_types unvarifyT
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S) | T => T);
@@ -572,11 +572,11 @@
 
 val legacy_varify =
   Term.map_aterms (fn Free (x, T) => Var ((x, 0), T) | t => t) #>
-  Term.map_term_types legacy_varifyT;
+  Term.map_types legacy_varifyT;
 
 val legacy_unvarify =
   Term.map_aterms (fn Var ((x, 0), T) => Free (x, T) | t => t) #>
-  Term.map_term_types legacy_unvarifyT;
+  Term.map_types legacy_unvarifyT;
 
 
 (* goal states *)
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/proofterm.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -604,7 +604,7 @@
       (case AList.lookup (op =) fmap f of
         NONE => TFree f
       | SOME b => TVar ((b, 0), S));
-  in map_proof_terms (map_term_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
+  in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf
   end;
 
 
@@ -630,7 +630,7 @@
       [] => prf (*nothing to do!*)
     | _ =>
       let val frzT = map_type_tvar (freeze_one alist)
-      in map_proof_terms (map_term_types frzT) frzT prf end)
+      in map_proof_terms (map_types frzT) frzT prf end)
   end;
 
 end;
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/sign.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -461,7 +461,7 @@
   let
     val _ = Context.check_thy thy;
     val _ = check_vars tm;
-    val tm' = Term.map_term_types (certify_typ thy) tm;
+    val tm' = Term.map_types (certify_typ thy) tm;
     val T = type_check pp tm';
     val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
     val tm'' = Consts.certify pp (tsig_of thy) consts tm';
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/term.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -68,7 +68,7 @@
   val map_aterms: (term -> term) -> term -> term
   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
   val map_type_tfree: (string * sort -> typ) -> typ -> typ
-  val map_term_types: (typ -> typ) -> term -> term
+  val map_types: (typ -> typ) -> term -> term
   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
@@ -423,7 +423,7 @@
 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
 
-fun map_term_types f =
+fun map_types f =
   let
     fun map_aux (Const (a, T)) = Const (a, f T)
       | map_aux (Free (a, T)) = Free (a, f T)
@@ -911,7 +911,7 @@
       in subst ty end;
 
 fun subst_atomic_types [] tm = tm
-  | subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm;
+  | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
 
 fun typ_subst_TVars [] ty = ty
   | typ_subst_TVars inst ty =
@@ -922,7 +922,7 @@
       in subst ty end;
 
 fun subst_TVars [] tm = tm
-  | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
+  | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
 
 fun subst_Vars [] tm = tm
   | subst_Vars inst tm =
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/thm.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -1138,7 +1138,7 @@
     val ((x, i), S) = Term.dest_TVar T handle TYPE _ =>
       raise THM ("unconstrainT: not a type variable", 0, [th]);
     val T' = TVar ((x, i), []);
-    val unconstrain = Term.map_term_types (Term.map_atyps (fn U => if U = T then T' else U));
+    val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
     val constraints = map (curry Logic.mk_inclass T') S;
   in
     Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/type.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -238,7 +238,7 @@
       (case AList.lookup (op =) fmap f of
         NONE => TFree f
       | SOME xi => TVar (xi, S));
-  in (map_term_types (map_type_tfree thaw) t, fmap) end;
+  in (map_types (map_type_tfree thaw) t, fmap) end;
 
 
 (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
@@ -277,8 +277,8 @@
   in
     (case alist of
       [] => (t, fn x => x) (*nothing to do!*)
-    | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
-      map_term_types (map_type_tfree (thaw_one (map swap alist)))))
+    | _ => (map_types (map_type_tvar (freeze_one alist)) t,
+      map_types (map_type_tfree (thaw_one (map swap alist)))))
   end;
 
 val freeze = #1 o freeze_thaw;
diff -r 796ae7fa1049 -r 8ef25fe585a8 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Sep 15 22:56:08 2006 +0200
+++ b/src/Pure/unify.ML	Fri Sep 15 22:56:13 2006 +0200
@@ -636,7 +636,7 @@
           Term.map_atyps (fn T as TVar ((x, i), S) =>
             if i > maxidx then TVar ((x, i - offset), S) else T | T => T);
         val decr_indexes =
-          Term.map_term_types decr_indexesT #>
+          Term.map_types decr_indexesT #>
           Term.map_aterms (fn t as Var ((x, i), T) =>
             if i > maxidx then Var ((x, i - offset), T) else t | t => t);