global typedef;

--- a/src/HOL/Import/proof_kernel.ML	Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOL/Import/proof_kernel.ML	Sat Mar 13 14:43:04 2010 +0100
@@ -2094,7 +2094,7 @@
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') =
-              Typedef.add_typedef false (SOME (Binding.name thmname))
+              Typedef.add_typedef_global false (SOME (Binding.name thmname))
                 (Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
 
@@ -2182,7 +2182,7 @@
             val tsyn = mk_syn thy tycname
             val typ = (tycname,tnames,tsyn)
             val ((_, typedef_info), thy') =
-              Typedef.add_typedef false NONE (Binding.name tycname,tnames,tsyn) c
+              Typedef.add_typedef_global false NONE (Binding.name tycname,tnames,tsyn) c
                 (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
             val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
             val fulltyname = Sign.intern_type thy' tycname

--- a/src/HOL/Import/replay.ML	Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOL/Import/replay.ML	Sat Mar 13 14:43:04 2010 +0100
@@ -343,7 +343,7 @@
           | delta (Hol_theorem (thyname, thmname, th)) thy =
             add_hol4_theorem thyname thmname ([], th_of thy th) thy
           | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
-            snd (Typedef.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
+            snd (Typedef.add_typedef_global false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c
         (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
           | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
             add_hol4_type_mapping thyname tycname true fulltyname thy

--- a/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sat Mar 13 14:43:04 2010 +0100
@@ -615,7 +615,7 @@
     val (typedefs, thy6) =
       thy4
       |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
-          Typedef.add_typedef false (SOME (Binding.name name'))
+          Typedef.add_typedef_global false (SOME (Binding.name name'))
             (Binding.name name, map fst tvs, mx)
             (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
                Const (cname, U --> HOLogic.boolT)) NONE

--- a/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sat Mar 13 14:43:04 2010 +0100
@@ -190,7 +190,7 @@
     val (typedefs, thy3) = thy2 |>
       Sign.parent_path |>
       fold_map (fn ((((name, mx), tvs), c), name') =>
-          Typedef.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
+          Typedef.add_typedef_global false (SOME (Binding.name name')) (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)

--- a/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Sat Mar 13 14:43:04 2010 +0100
@@ -75,7 +75,7 @@
      EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
 in
   Local_Theory.theory_result
-    (Typedef.add_typedef false NONE
+    (Typedef.add_typedef_global false NONE
        (qty_name, vs, mx)
           (typedef_term rel rty lthy)
              NONE typedef_tac) lthy

--- a/src/HOL/Tools/record.ML	Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOL/Tools/record.ML	Sat Mar 13 14:43:04 2010 +0100
@@ -104,8 +104,8 @@
   let
     fun get_thms thy name =
       let
-        val {Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
-          Abs_inverse = abs_inverse, ...} = Typedef.the_info thy name;
+        val [{Rep_inject = rep_inject, Abs_name = absN, abs_type = absT,
+          Abs_inverse = abs_inverse, ...}] = Typedef.get_info_global thy name;
         val rewrite_rule =
           MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
       in

--- a/src/HOLCF/Tools/pcpodef.ML	Sat Mar 13 14:42:16 2010 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Sat Mar 13 14:43:04 2010 +0100
@@ -181,7 +181,7 @@
   let
     val name = the_default (#1 typ) opt_name;
     val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy
-      |> Typedef.add_typedef def opt_name typ set opt_morphs tac;
+      |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
     val oldT = #rep_type info;
     val newT = #abs_type info;
     val lhs_tfrees = map dest_TFree (snd (dest_Type newT));