| changeset 44689 | f247fc952f31 |
| parent 44045 | 2814ff2a6e3e |
| child 44868 | 92be5b32ca71 |
--- a/src/HOL/Nominal/nominal_inductive.ML Sat Sep 03 23:38:06 2011 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Sep 03 23:59:36 2011 +0200 @@ -32,7 +32,7 @@ val fresh_prod = @{thm fresh_prod}; -val perm_bool = mk_meta_eq @{thm perm_bool}; +val perm_bool = mk_meta_eq @{thm perm_bool_def}; val perm_boolI = @{thm perm_boolI}; val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb (Drule.strip_imp_concl (cprop_of perm_boolI))));