# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258672832 -3600
# Node ID b6a1feca2ac207ed01cfe709bdd4d36026203289
# Parent  17926df64f0f420b85e5a9a161de78d4e9edc648
use of thm-antiquotation

diff -r 17926df64f0f -r b6a1feca2ac2 src/HOL/Nominal/nominal_inductive.ML
--- 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 [];
 
diff -r 17926df64f0f -r b6a1feca2ac2 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Nov 19 16:07:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.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 [];