src/HOL/Nominal/nominal_fresh_fun.ML
changeset 55951 c07d184aebe9
parent 51717 9e7d1c139569
child 55952 2f85cc6c27d4
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 11:32:16 2014 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 06 12:10:19 2014 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4       (Scan.succeed false);
     1.5  
     1.6  fun setup_generate_fresh x =
     1.7 -  (Args.goal_spec -- Args.type_name true >>
     1.8 +  (Args.goal_spec -- Args.type_name {proper = false, strict = 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 =