changeset 44689 | f247fc952f31 |
parent 44241 | 7943b69f0188 |
child 44868 | 92be5b32ca71 |
--- a/src/HOL/Nominal/nominal_inductive2.ML Sat Sep 03 23:38:06 2011 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Sep 03 23:59:36 2011 +0200 @@ -36,7 +36,7 @@ fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps; -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))));