--- a/src/HOL/Nominal/nominal_inductive.ML Thu Nov 19 16:07:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Nov 20 00:20:32 2009 +0100
@@ -15,9 +15,9 @@
struct
val inductive_forall_name = "HOL.induct_forall";
-val inductive_forall_def = thm "induct_forall_def";
-val inductive_atomize = thms "induct_atomize";
-val inductive_rulify = thms "induct_rulify";
+val inductive_forall_def = @{thm induct_forall_def};
+val inductive_atomize = @{thms induct_atomize};
+val inductive_rulify = @{thms induct_rulify};
fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];