--- a/src/HOL/Nominal/nominal_inductive.ML Mon Sep 06 19:11:01 2010 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Mon Sep 06 19:13:10 2010 +0200
@@ -30,10 +30,10 @@
fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
-val fresh_prod = thm "fresh_prod";
+val fresh_prod = @{thm fresh_prod};
-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))));