# HG changeset patch
# User wenzelm
# Date 1320848319 -3600
# Node ID 01d75cf044979de7049bb90fce77487126ed772d
# Parent  92f91f990165ed3323401751b2882f2221275b59
localized Record.decode_type: use standard Proof_Context.get_sort;
clarified Record.varifyT: more convential use of maxidx + 1;

diff -r 92f91f990165 -r 01d75cf04497 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Wed Nov 09 14:58:48 2011 +0100
+++ b/src/HOL/Tools/record.ML	Wed Nov 09 15:18:39 2011 +0100
@@ -249,9 +249,7 @@
 
 (*** utilities ***)
 
-fun varifyT midx =
-  let fun varify (a, S) = TVar ((a, midx + 1), S);
-  in map_type_tfree varify end;
+fun varifyT idx = map_type_tfree (fn (a, S) => TVar ((a, idx), S));
 
 
 (* timing *)
@@ -582,8 +580,7 @@
     val recname =
       let val (nm :: _ :: rst) = rev (Long_Name.explode name)   (* FIXME !? *)
       in Long_Name.implode (rev (nm :: rst)) end;
-    val midx = maxidx_of_typs (moreT :: Ts);
-    val varifyT = varifyT midx;
+    val varifyT = varifyT (maxidx_of_typs (moreT :: Ts) + 1);
     val {records, extfields, ...} = Data.get thy;
     val (fields, (more, _)) = split_last (Symtab.lookup_list extfields name);
     val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
@@ -657,13 +654,8 @@
 
 (* decode type *)
 
-fun decode_type thy t =
-  let
-    fun get_sort env xi =
-      the_default (Sign.defaultS thy) (AList.lookup (op =) env (xi: indexname));
-  in
-    Syntax_Phases.typ_of_term (get_sort (Syntax_Phases.term_sorts t)) t
-  end;
+fun decode_type ctxt t =
+  Syntax_Phases.typ_of_term (Proof_Context.get_sort ctxt (Syntax_Phases.term_sorts t)) t;
 
 
 (* parse translations *)
@@ -702,9 +694,8 @@
                     val types = map snd fields';
                     val (args, rest) = split_args (map fst fields') fargs
                       handle Fail msg => err msg;
-                    val argtypes = map (Sign.certify_typ thy o decode_type thy) args;
-                    val midx = fold Term.maxidx_typ argtypes 0;
-                    val varifyT = varifyT midx;
+                    val argtypes = map (Syntax.check_typ ctxt o decode_type ctxt) args;
+                    val varifyT = varifyT (fold Term.maxidx_typ argtypes 0 + 1);
                     val vartypes = map varifyT types;
 
                     val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
@@ -808,8 +799,8 @@
   let
     val thy = Proof_Context.theory_of ctxt;
 
-    val T = decode_type thy t;
-    val varifyT = varifyT (Term.maxidx_of_typ T);
+    val T = decode_type ctxt t;
+    val varifyT = varifyT (Term.maxidx_of_typ T + 1);
 
     fun strip_fields T =
       (case T of
@@ -853,10 +844,8 @@
   the (nested) extension types*)
 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val T = decode_type thy tm;
-    val midx = maxidx_of_typ T;
-    val varifyT = varifyT midx;
+    val T = decode_type ctxt tm;
+    val varifyT = varifyT (maxidx_of_typ T + 1);
 
     fun mk_type_abbr subst name args =
       let val abbrT = Type (name, map (varifyT o TFree) args)