src/HOL/Nominal/nominal_package.ML
changeset 19874 cc4b2b882e4c
parent 19851 10162c01bd78
child 19985 d39c554cf750
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Jun 13 23:41:31 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Jun 13 23:41:34 2006 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  val meta_spec = thm "meta_spec";
     1.5  
     1.6  fun projections rule =
     1.7 -  ProjectRule.projections rule
     1.8 +  ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
     1.9    |> map (standard #> RuleCases.save rule);
    1.10  
    1.11  fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =