changeset 27153 | 56b6cdce22f1 |
parent 27112 | 661a74bafeb7 |
child 27228 | 4f7976a6ffc3 |
--- a/src/HOL/Nominal/nominal_package.ML Wed Jun 11 18:01:36 2008 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Wed Jun 11 18:02:00 2008 +0200 @@ -155,7 +155,7 @@ val perm_simproc = Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc'; -val allE_Nil = read_instantiate_sg (the_context()) [("x", "[]")] allE; +val allE_Nil = Drule.read_instantiate_sg (the_context()) [("x", "[]")] allE; val meta_spec = thm "meta_spec";