src/HOL/Nominal/nominal_fresh_fun.ML
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 32149 ef59550a55d3
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -199,9 +199,10 @@
     1.4      (Args.parens (Args.$$$ "no_asm") >> (K true)) ||
     1.5       (Scan.succeed false);
     1.6  
     1.7 -val setup_generate_fresh =
     1.8 -  Method.goal_args_ctxt' Args.tyname (fn ctxt => generate_fresh_tac) 
     1.9 +fun setup_generate_fresh x =
    1.10 +  (Args.goal_spec -- Args.tyname >>
    1.11 +    (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
    1.12  
    1.13 -val setup_fresh_fun_simp =
    1.14 -  Method.simple_args options_syntax 
    1.15 -  (fn b => fn _ => SIMPLE_METHOD (fresh_fun_tac b 1))
    1.16 +fun setup_fresh_fun_simp x =
    1.17 +  (Scan.lift options_syntax >> (fn b => K (SIMPLE_METHOD' (fresh_fun_tac b)))) x;
    1.18 +