| changeset 32010 | cb1a1c94b4cd |
| parent 31936 | 9466169dc8e0 |
| child 32124 | 954321008785 |
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Jul 15 23:11:57 2009 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Jul 15 23:48:21 2009 +0200 @@ -147,7 +147,7 @@ | perm_simproc' thy ss _ = NONE; val perm_simproc = - Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc'; + Simplifier.simproc @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc'; val meta_spec = thm "meta_spec";