| changeset 25985 | 8d69087f6a4b |
| parent 25977 | b0604cd8e5e1 |
| child 25998 | f38dc602a926 |
--- a/src/HOL/Nominal/nominal_package.ML Sat Jan 26 17:08:43 2008 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Sat Jan 26 20:01:37 2008 +0100 @@ -153,7 +153,7 @@ | perm_simproc' thy ss _ = NONE; val perm_simproc = - Simplifier.simproc (the_context ()) "perm_simp" ["pi1 \\<bullet> (pi2 \\<bullet> x)"] 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;