src/HOL/Nominal/nominal_primrec.ML

     val used = map fst (fold Term.add_frees fs []);
     val x = (Name.variant used "x", dummyT);
     val frees = ls @ x :: rs;
     val raw_rhs = list_abs_free (frees,
       list_comb (Const (rec_name, dummyT), fs @ [Free x]))
-    val def_name = Thm.def_name (Sign.base_name fname);
+    val def_name = Thm.def_name (NameSpace.base_name fname);
     val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
     val SOME var = get_first (fn ((b, _), mx) =>
       if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
   in
     ((var, ((Binding.name def_name, []), rhs)),

     val (defs_thms, lthy') = lthy |>
       set_group ? LocalTheory.set_group (serial_string ()) |>
       fold_map (apfst (snd o snd) oo
         LocalTheory.define Thm.definitionK o fst) defs';
     val qualify = Binding.qualify false
-      (space_implode "_" (map (Sign.base_name o #1) defs));
+      (space_implode "_" (map (NameSpace.base_name o #1) defs));
     val names_atts' = map (apfst qualify) names_atts;
     val cert = cterm_of (ProofContext.theory_of lthy');
 
     fun mk_idx eq =
       let