src/HOL/Nominal/nominal_inductive.ML
changeset 44689 f247fc952f31
parent 44045 2814ff2a6e3e
child 44868 92be5b32ca71
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sat Sep 03 23:38:06 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sat Sep 03 23:59:36 2011 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5  val fresh_prod = @{thm fresh_prod};
     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))));