src/HOL/Nominal/nominal_fresh_fun.ML
changeset 35360 df2b2168e43a
parent 34885 6587c24ef6d8
child 35667 aa59452c913c
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Feb 25 22:05:34 2010 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Feb 25 22:06:43 2010 +0100
     1.3 @@ -182,7 +182,7 @@
     1.4       (Scan.succeed false);
     1.5  
     1.6  fun setup_generate_fresh x =
     1.7 -  (Args.goal_spec -- Args.tyname >>
     1.8 +  (Args.goal_spec -- Args.type_name true >>
     1.9      (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
    1.10  
    1.11  fun setup_fresh_fun_simp x =