src/HOL/Nominal/nominal_induct.ML
changeset 30092 9c3b1c136d1f
parent 29581 b3b33e0298eb
child 30510 4120fc59dd85
     1.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Feb 25 18:53:34 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Feb 25 19:34:00 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4 -(*  ID:         $Id$
     1.5 -    Author:     Christian Urban and Makarius
     1.6 +(*  Author:     Christian Urban and Makarius
     1.7  
     1.8  The nominal induct proof method.
     1.9  *)
    1.10 @@ -24,7 +23,8 @@
    1.11  
    1.12  val split_all_tuples =
    1.13    Simplifier.full_simplify (HOL_basic_ss addsimps
    1.14 -    [split_conv, split_paired_all, unit_all_eq1, thm "fresh_unit_elim", thm "fresh_prod_elim"]);
    1.15 +    [split_conv, split_paired_all, unit_all_eq1, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @
    1.16 +    @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim});
    1.17  
    1.18  
    1.19  (* prepare rule *)