some localization;

--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 15:23:27 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Dec 02 16:24:48 2011 +0100
@@ -682,6 +682,7 @@
     val tmp_thy = thy
       |> Theory.copy
       |> Sign.add_types_global (map (fn (tvs, tname, mx, _) => (tname, length tvs, mx)) dts);
+    val tmp_ctxt = Proof_Context.init_global tmp_thy;
 
     val (tyvars, _, _, _) ::_ = dts;
     val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
@@ -732,7 +733,7 @@
     val sorts =
       sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
     val dt_info = Datatype_Data.get_all thy;
-    val (descr, _) = Datatype_Aux.unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
+    val (descr, _) = Datatype_Aux.unfold_datatypes tmp_ctxt dts' sorts dt_info dts' i;
     val _ =
       Datatype_Aux.check_nonempty descr
         handle (exn as Datatype_Aux.Datatype_Empty s) =>

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 02 15:23:27 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Dec 02 16:24:48 2011 +0100
@@ -76,7 +76,7 @@
     -> ((string * typ list) * (string * 'a list) list) list
   val check_nonempty : descr list -> unit
   val unfold_datatypes :
-    theory -> descr -> (string * sort) list -> info Symtab.table ->
+    Proof.context -> descr -> (string * sort) list -> info Symtab.table ->
       descr -> int -> descr list * int
   val find_shortest_path : descr -> int -> (string * int) option
 end;
@@ -323,11 +323,11 @@
 (* all types of the form DtType (dt_name, [..., DtRec _, ...]) *)
 (* need to be unfolded                                         *)
 
-fun unfold_datatypes thy orig_descr sorts (dt_info : info Symtab.table) descr i =
+fun unfold_datatypes ctxt orig_descr sorts (dt_info : info Symtab.table) descr i =
   let
     fun typ_error T msg =
       error ("Non-admissible type expression\n" ^
-        Syntax.string_of_typ_global thy (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
+        Syntax.string_of_typ ctxt (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
 
     fun get_dt_descr T i tname dts =
       (case Symtab.lookup dt_info tname of
@@ -359,7 +359,7 @@
                 let
                   val (index, descr) = get_dt_descr T i tname dts;
                   val (descr', i') =
-                    unfold_datatypes thy orig_descr sorts dt_info descr (i + length descr);
+                    unfold_datatypes ctxt orig_descr sorts dt_info descr (i + length descr);
                 in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
             | _ => (i, Ts @ [T], descrs))
         end