src/HOL/Nominal/nominal_inductive2.ML
changeset 44689 f247fc952f31
parent 44241 7943b69f0188
child 44868 92be5b32ca71
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Sep 03 23:38:06 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Sep 03 23:59:36 2011 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
     1.6  
     1.7 -val perm_bool = mk_meta_eq @{thm perm_bool};
     1.8 +val perm_bool = mk_meta_eq @{thm perm_bool_def};
     1.9  val perm_boolI = @{thm perm_boolI};
    1.10  val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
    1.11    (Drule.strip_imp_concl (cprop_of perm_boolI))));