# HG changeset patch
# User wenzelm
# Date 1271440684 -7200
# Node ID 99212848c93305534efc702d454d012956f01127
# Parent  fc407d02af4a5cf3a1b4a1504f1f5e6464b32914
modernized type abbreviations;

diff -r fc407d02af4a -r 99212848c933 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Fri Apr 16 19:43:06 2010 +0200
+++ b/src/HOL/Tools/record.ML	Fri Apr 16 19:58:04 2010 +0200
@@ -1971,11 +1971,6 @@
 
     (* prepare definitions *)
 
-    (*record (scheme) type abbreviation*)
-    val recordT_specs =
-      [(Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), rec_schemeT0, NoSyn),
-        (binding, map #1 alphas, recT0, NoSyn)];
-
     val ext_defs = ext_def :: map #ext_def parents;
 
     (*Theorems from the iso_tuple intros.
@@ -2059,7 +2054,9 @@
       ext_thy
       |> Sign.add_advanced_trfuns ([], [], advanced_print_translation, [])
       |> Sign.restore_naming thy
-      |> Sign.add_tyabbrs_i recordT_specs
+      |> Typedecl.abbrev_global (binding, map #1 alphas, NoSyn) recT0 |> snd
+      |> Typedecl.abbrev_global
+        (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
       |> Sign.qualified_path false binding
       |> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx))
         (sel_decls ~~ (field_syntax @ [NoSyn]))