src/HOL/Nominal/nominal_fresh_fun.ML
changeset 30510 4120fc59dd85
parent 30364 577edc39b501
child 30549 d2d7874648bd
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -204,4 +204,4 @@
     1.4  
     1.5  val setup_fresh_fun_simp =
     1.6    Method.simple_args options_syntax 
     1.7 -  (fn b => fn _ => Method.SIMPLE_METHOD (fresh_fun_tac b 1))
     1.8 +  (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))