src/HOL/Nominal/nominal_inductive2.ML

     [@{thm fresh_star_set_eq}, @{thm fresh_star_Un_elim},
      @{thm fresh_star_insert_elim}, @{thm fresh_star_empty_elim}]);
 
 fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
 
-val perm_bool = mk_meta_eq (thm "perm_bool");
-val perm_boolI = thm "perm_boolI";
+val perm_bool = mk_meta_eq @{thm perm_bool};
+val perm_boolI = @{thm perm_boolI};
 val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
   (Drule.strip_imp_concl (cprop_of perm_boolI))));
 
 fun mk_perm_bool pi th = th RS Drule.cterm_instantiate
   [(perm_boolI_pi, pi)] perm_boolI;