diff -r 588329441a78 -r cc4b2b882e4c src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Tue Jun 13 23:41:31 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Tue Jun 13 23:41:34 2006 +0200
@@ -133,7 +133,7 @@
 val meta_spec = thm "meta_spec";
 
 fun projections rule =
-  ProjectRule.projections rule
+  ProjectRule.projections (ProofContext.init (Thm.theory_of_thm rule)) rule
   |> map (standard #> RuleCases.save rule);
 
 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =