use of thm-antiquotation
authorChristian Urban <urbanc@in.tum.de>
Fri Nov 20 00:20:32 2009 +0100 (2009-11-20)
changeset 33772b6a1feca2ac2
parent 33771 17926df64f0f
child 33773 ccef2e6d8c21
use of thm-antiquotation
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Nov 19 16:07:53 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Nov 20 00:20:32 2009 +0100
     1.3 @@ -15,9 +15,9 @@
     1.4  struct
     1.5  
     1.6  val inductive_forall_name = "HOL.induct_forall";
     1.7 -val inductive_forall_def = thm "induct_forall_def";
     1.8 -val inductive_atomize = thms "induct_atomize";
     1.9 -val inductive_rulify = thms "induct_rulify";
    1.10 +val inductive_forall_def = @{thm induct_forall_def};
    1.11 +val inductive_atomize = @{thms induct_atomize};
    1.12 +val inductive_rulify = @{thms induct_rulify};
    1.13  
    1.14  fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
    1.15  
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Nov 19 16:07:53 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Nov 20 00:20:32 2009 +0100
     2.3 @@ -15,9 +15,9 @@
     2.4  struct
     2.5  
     2.6  val inductive_forall_name = "HOL.induct_forall";
     2.7 -val inductive_forall_def = thm "induct_forall_def";
     2.8 -val inductive_atomize = thms "induct_atomize";
     2.9 -val inductive_rulify = thms "induct_rulify";
    2.10 +val inductive_forall_def = @{thm induct_forall_def};
    2.11 +val inductive_atomize = @{thms induct_atomize};
    2.12 +val inductive_rulify = @{thms induct_rulify};
    2.13  
    2.14  fun rulify_term thy = MetaSimplifier.rewrite_term thy inductive_rulify [];
    2.15