src/HOL/Tools/datatype_prop.ML

 
   in (rec_result_Ts, reccomb_fn_Ts) end;
 
 fun make_primrecs new_type_names descr sorts thy =
   let
-    val sign = Theory.sign_of thy;
-
     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
     val used = foldr add_typ_tfree_names [] recTs;
 
     val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
 
     val rec_fns = map (uncurry (mk_Free "f"))
       (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
 
     val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
-    val reccomb_names = map (Sign.intern_const sign)
+    val reccomb_names = map (Sign.intern_const thy)
       (if length descr' = 1 then [big_reccomb_name] else
         (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
           (1 upto (length descr'))));
     val reccombs = map (fn ((name, T), T') => list_comb
       (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))

       map (fn (_, cargs) =>
         let val Ts = map (typ_of_dtyp descr' sorts) cargs
         in Ts ---> T' end) constrs) (hd descr);
 
     val case_names = map (fn s =>
-      Sign.intern_const (Theory.sign_of thy) (s ^ "_case")) new_type_names
+      Sign.intern_const thy (s ^ "_case")) new_type_names
   in
     map (fn ((name, Ts), T) => list_comb
       (Const (name, Ts @ [T] ---> T'),
         map (uncurry (mk_Free fname)) (Ts ~~ (1 upto length Ts))))
           (case_names ~~ case_fn_Ts ~~ newTs)

     val descr' = List.concat descr;
     val recTs = get_rec_types descr' sorts;
 
     val size_name = "Nat.size";
     val size_names = replicate (length (hd descr)) size_name @
-      map (Sign.intern_const (Theory.sign_of thy)) (indexify_names
+      map (Sign.intern_const thy) (indexify_names
         (map (fn T => name_of_typ T ^ "_size") (Library.drop (length (hd descr), recTs))));
     val size_consts = map (fn (s, T) =>
       Const (s, T --> HOLogic.natT)) (size_names ~~ recTs);
 
     fun plus (t1, t2) = Const ("HOL.plus", [HOLogic.natT, HOLogic.natT] ---> HOLogic.natT) $ t1 $ t2;