src/Pure/sign.ML

 fun read_raw_typ (sg, def_sort) = read_raw_typ' (syn_of sg) (sg, def_sort);
 
 (*read and certify typ wrt a signature*)
 local
   fun read_typ_aux rd cert (sg, def_sort) str =
-    (cert (tsig_of sg) (rd (sg, def_sort) str)
+    (#1 (cert (tsig_of sg) (rd (sg, def_sort) str))
       handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
 in
   val read_typ          = read_typ_aux read_raw_typ Type.cert_typ;
   val read_typ_raw      = read_typ_aux read_raw_typ Type.cert_typ_raw;
   fun read_typ' syn     = read_typ_aux (read_raw_typ' syn) Type.cert_typ;

 
 (** certify classes, sorts, types and terms **)   (*exception TYPE*)
 
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
-val certify_typ = Type.cert_typ o tsig_of;
-val certify_typ_raw = Type.cert_typ_raw o tsig_of;
+val certify_typ = #1 oo (Type.cert_typ o tsig_of);
+val certify_typ_raw = #1 oo (Type.cert_typ_raw o tsig_of);
 
 fun certify_tyname sg c =
   if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c
   else raise TYPE ("Undeclared type constructor: " ^ quote c, [], []);
 

   if is_some (const_type sg c) then c
   else raise TYPE ("Undeclared constant: " ^ quote c, [], []);
 
 
 (* certify_term *)
+
+local
+
+(*certify types of term and compute maxidx*)
+fun cert_term_types certT =
+  let
+    fun cert (Const (a, T)) = let val (T', i) = certT T in (Const (a, T'), i) end
+      | cert (Free (a, T)) = let val (T', i) = certT T in (Free (a, T'), i) end
+      | cert (Var (xi as (_, i), T)) =
+          let val (T', j) = certT T in (Var (xi, T'), Int.max (i, j)) end
+      | cert (t as Bound _) = (t, ~1)
+      | cert (Abs (a, T, t)) =
+          let val (T', i) = certT T and (t', j) = cert t
+          in (Abs (a, T', t'), Int.max (i, j)) end
+      | cert (t $ u) =
+          let val (t', i) = cert t and (u', j) =  cert u
+          in (t' $ u', Int.max (i, j)) end;
+  in cert end;
+
+(*compute and check type of the term*)
+fun type_check pp sg tm =
+  let
+    fun err_appl why bs t T u U =
+      let
+        val xs = map Free bs;           (*we do not rename here*)
+        val t' = subst_bounds (xs, t);
+        val u' = subst_bounds (xs, u);
+        val text = cat_lines
+          (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
+      in raise TYPE (text, [T, U], [t', u']) end;
+
+    fun typ_of (_, Const (_, T)) = T
+      | typ_of (_, Free  (_, T)) = T
+      | typ_of (_, Var (_, T)) = T
+      | typ_of (bs, Bound i) = snd (nth_elem (i, bs) handle LIST _ =>
+          raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
+      | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
+      | typ_of (bs, t $ u) =
+          let val T = typ_of (bs, t) and U = typ_of (bs, u) in
+            (case T of
+              Type ("fun", [T1, T2]) =>
+                if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
+            | _ => err_appl "Operator not of function type" bs t T u U)
+          end;
+
+  in typ_of ([], tm) end;
 
 (*check for duplicate occurrences of TFree/TVar with distinct sorts*)
 fun nodup_tvars (env, Type (_, Ts)) = nodup_tvars_list (env, Ts)
   | nodup_tvars (env as (tfrees, tvars), T as TFree (v as (a, S))) =
       (case assoc_string (tfrees, a) of

             " has two distinct sorts", [TVar (a, S'), T], [])
       | None => (tfrees, v :: tvars))
 (*equivalent to foldl nodup_tvars_list, but 3X faster under Poly/ML*)
 and nodup_tvars_list (env, []) = env
   | nodup_tvars_list (env, T :: Ts) = nodup_tvars_list (nodup_tvars (env, T), Ts);
+
+in
 
 (*check for duplicate occurrences of Free/Var with distinct types*)
 fun nodup_vars tm =
   let
     fun nodups (envs as (env as (frees, vars), envT)) tm =

       | Bound _ => envs
       | Abs (_, T, t) => nodups (env, nodup_tvars (envT, T)) t
       | s $ t => nodups (nodups envs s) t)
   in nodups (([], []), ([], [])) tm; tm end;
 
-(*compute and check type of the term*)
-fun type_check pp sg tm =
-  let
-    fun err_appl why bs t T u U =
-      let
-        val xs = map Free bs;           (*we do not rename here*)
-        val t' = subst_bounds (xs, t);
-        val u' = subst_bounds (xs, u);
-        val text = cat_lines
-          (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
-      in raise TYPE (text, [T, U], [t', u']) end;
-
-    fun typ_of (_, Const (_, T)) = T
-      | typ_of (_, Free  (_, T)) = T
-      | typ_of (_, Var (_, T)) = T
-      | typ_of (bs, Bound i) = snd (nth_elem (i, bs) handle LIST _ =>
-          raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
-      | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
-      | typ_of (bs, t $ u) =
-          let val T = typ_of (bs, t) and U = typ_of (bs, u) in
-            (case T of
-              Type ("fun", [T1, T2]) =>
-                if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
-            | _ => err_appl "Operator not of function type" bs t T u U)
-          end;
-
-  in typ_of ([], tm) end;
-
 fun certify_term pp sg tm =
   let
     val _ = check_stale sg;
 
-    val tm' = Term.map_term_types (Type.cert_typ (tsig_of sg)) tm;
+    val (tm', maxidx) = cert_term_types (Type.cert_typ (tsig_of sg)) tm;
     val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
 
     fun err msg = raise TYPE (msg, [], [tm']);
 
     fun show_const a T = quote a ^ " :: " ^ Pretty.string_of_typ pp T;

           if i < 0 then err ("Malformed variable: " ^ quote x) else ()
       | check_atoms _ = ();
   in
     check_atoms tm';
     nodup_vars tm';
-    (tm', type_check pp sg tm', maxidx_of_term tm')
-  end;
+    (tm', type_check pp sg tm', maxidx)
+  end;
+
+end;
 
 
 
 (** instantiation **)
 

 
 fun ext_cnsts rd_const syn_only prmode sg (syn, tsig, ctab, (path, spaces), data)
     raw_consts =
   let
     val prep_typ = compress_type o Type.varifyT o Type.no_tvars o
-      (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig);
+     (if syn_only then #1 o Type.cert_typ_syntax tsig
+      else Term.no_dummyT o #1 o Type.cert_typ tsig);
     fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) =>
       (error_msg msg; err_in_const (const_name path c mx));
 
     val consts = map (prep_const o rd_const sg syn tsig (path, spaces)) raw_consts;
     val decls =