src/HOL/Nominal/nominal_inductive.ML
changeset 33772 b6a1feca2ac2
parent 33671 4b0f2599ed48
child 33968 f94fb13ecbb3
     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