export read_typ/cert_typ -- version with regular context operations;
tuned;

--- a/src/HOL/Tools/record_package.ML	Thu Jun 19 20:48:01 2008 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Jun 19 20:48:02 2008 +0200
@@ -43,6 +43,8 @@
   val get_extinjects: theory -> thm list
   val get_simpset: theory -> simpset
   val print_records: theory -> unit
+  val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list
+  val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list
   val add_record: bool -> string list * string -> string option -> (string * string * mixfix) list
     -> theory -> theory
   val add_record_i: bool -> string list * string -> (typ list * string) option
@@ -1378,22 +1380,25 @@
 
 (* prepare arguments *)
 
-fun read_raw_parent sign s =
-  (case Sign.read_typ_abbrev sign s handle TYPE (msg, _, _) => error msg of
+fun read_raw_parent ctxt raw_T =
+  (case ProofContext.read_typ_abbrev ctxt raw_T of
     Type (name, Ts) => (Ts, name)
-  | _ => error ("Bad parent record specification: " ^ quote s));
+  | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
 
-fun read_typ sign (env, s) =
+fun read_typ ctxt raw_T env =
   let
-    fun def_sort (x, ~1) = AList.lookup (op =) env x
-      | def_sort _ = NONE;
-    val T = Type.no_tvars (Sign.read_def_typ (sign, def_sort) s)
-      handle TYPE (msg, _, _) => error msg;
-  in (Term.add_typ_tfrees (T, env), T) end;
+    val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
+    val T = Syntax.read_typ ctxt' raw_T;
+    val env' = Term.add_typ_tfrees (T, env);
+  in (T, env') end;
 
-fun cert_typ sign (env, raw_T) =
-  let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg
-  in (Term.add_typ_tfrees (T, env), T) end;
+fun cert_typ ctxt raw_T env =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val T = Type.no_tvars (Sign.certify_typ thy raw_T) handle TYPE (msg, _, _) => error msg;
+    val env' = Term.add_typ_tfrees (T, env);
+  in (T, env') end;
+
 
 (* attributes *)
 
@@ -2202,6 +2207,7 @@
   in final_thy
   end;
 
+
 (* add_record *)
 
 (*we do all preparations and error checks here, deferring the real
@@ -2211,12 +2217,14 @@
     val _ = Theory.requires thy "Record" "record definitions";
     val _ = if quiet_mode then () else writeln ("Defining record " ^ quote bname ^ " ...");
 
+    val ctxt = ProofContext.init thy;
+
 
     (* parents *)
 
-    fun prep_inst T = snd (cert_typ thy ([], T));
+    fun prep_inst T = fst (cert_typ ctxt T []);
 
-    val parent = Option.map (apfst (map prep_inst) o prep_raw_parent thy) raw_parent
+    val parent = Option.map (apfst (map prep_inst) o prep_raw_parent ctxt) raw_parent
       handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
     val parents = add_parents thy parent [];
 
@@ -2228,12 +2236,12 @@
 
     (* fields *)
 
-    fun prep_field (env, (c, raw_T, mx)) =
-      let val (env', T) = prep_typ thy (env, raw_T) handle ERROR msg =>
-        cat_error msg ("The error(s) above occured in field " ^ quote c)
-      in (env', (c, T, mx)) end;
+    fun prep_field (c, raw_T, mx) env =
+      let val (T, env') = prep_typ ctxt raw_T env handle ERROR msg =>
+        cat_error msg ("The error(s) above occured in record field " ^ quote c)
+      in ((c, T, mx), env') end;
 
-    val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
+    val (bfields, envir) = fold_map prep_field raw_fields init_env;
     val envir_names = map fst envir;