src/HOL/Tools/record_package.ML

 (* parent records *)
 
 fun add_parents thy NONE parents = parents
   | add_parents thy (SOME (types, name)) parents =
       let
-        val sign = Theory.sign_of thy;
         fun err msg = error (msg ^ " parent record " ^ quote name);
 
         val {args, parent, fields, extension, induct} =
           (case get_record thy name of SOME info => info | NONE => err "Unknown");
         val _ = if length types <> length args then err "Bad number of arguments for" else ();
 
         fun bad_inst ((x, S), T) =
-          if Sign.of_sort sign (T, S) then NONE else SOME x
+          if Sign.of_sort thy (T, S) then NONE else SOME x
         val bads = List.mapPartial bad_inst (args ~~ types);
         val _ = null bads orelse err ("Ill-sorted instantiation of " ^ commas bads ^ " in");
 
         val inst = map fst args ~~ types;
         val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst);

 
 (* record_definition *)
 fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy =
   (* smlnj needs type annotation of parents *)
   let
-    val sign = Theory.sign_of thy;
-
     val alphas = map fst args;
-    val name = Sign.full_name sign bname;
-    val full = Sign.full_name_path sign bname;
+    val name = Sign.full_name thy bname;
+    val full = Sign.full_name_path thy bname;
     val base = Sign.base_name;
 
     val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
 
     val parent_fields = List.concat (map #fields parents);

 (*we do all preparations and error checks here, deferring the real
   work to record_definition*)
 fun gen_add_record prep_typ prep_raw_parent (params, bname) raw_parent raw_fields thy =
   let
     val _ = Theory.requires thy "Record" "record definitions";
-    val sign = Theory.sign_of thy;
     val _ = message ("Defining record " ^ quote bname ^ " ...");
 
 
     (* parents *)
 
-    fun prep_inst T = snd (cert_typ sign ([], T));
-
-    val parent = Option.map (apfst (map prep_inst) o prep_raw_parent sign) raw_parent
+    fun prep_inst T = snd (cert_typ thy ([], T));
+
+    val parent = Option.map (apfst (map prep_inst) o prep_raw_parent thy) raw_parent
       handle ERROR msg => cat_error msg ("The error(s) above in parent record specification");
     val parents = add_parents thy parent [];
 
     val init_env =
       (case parent of

 
 
     (* fields *)
 
     fun prep_field (env, (c, raw_T, mx)) =
-      let val (env', T) = prep_typ sign (env, raw_T) handle ERROR msg =>
+      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;
 
     val (envir, bfields) = foldl_map prep_field (init_env, raw_fields);
     val envir_names = map fst envir;
 
 
     (* args *)
 
-    val defaultS = Sign.defaultS sign;
+    val defaultS = Sign.defaultS thy;
     val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params;
 
 
     (* errors *)
 
-    val name = Sign.full_name sign bname;
+    val name = Sign.full_name thy bname;
     val err_dup_record =
       if is_none (get_record thy name) then []
       else ["Duplicate definition of record " ^ quote name];
 
     val err_dup_parms =