src/HOL/Tools/datatype_package.ML

         let val Ts = map (typ_of_dtyp descr' sorts) cargs
         in Ts ---> freeT end) constrs) (hd descr);
 
     val case_names = map (fn s => (s ^ "_case")) new_type_names;
 
-    val thy2 = thy |>
+    val thy2' = thy |>
 
       (** new types **)
 
       curry (foldr (fn (((name, mx), tvs), thy') => thy' |>
         PureThy.add_typedecls [(name, tvs, mx)] |>

       (** case combinators **)
 
       Theory.add_consts_i (map (fn ((name, T), Ts) =>
         (name, Ts @ [T] ---> freeT, NoSyn))
           (case_names ~~ newTs ~~ case_fn_Ts)) |>
-      Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr) |>
+      Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr);
+
+    val reccomb_names' = map (Sign.intern_const (sign_of thy2')) reccomb_names;
+    val case_names' = map (Sign.intern_const (sign_of thy2')) case_names;
+
+    val thy2 = thy2' |>
 
       (** t_ord functions **)
 
       Theory.add_consts_i
         (foldr (fn ((((_, (_, _, constrs)), tname), T), decls) =>

     val (thy9, nchotomys) = add_and_get_axioms "nchotomy" new_type_names
       (DatatypeProp.make_nchotomys descr sorts) thy8;
     val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
       (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
     
-    val dt_infos = map (make_dt_info descr' induct reccomb_names rec_thms)
-      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
+    val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
+      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
         exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
     val thy11 = thy10 |>