src/HOL/Nominal/nominal_fresh_fun.ML
changeset 34885 6587c24ef6d8
parent 33040 cffdb7b28498
child 35360 df2b2168e43a
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Tue Jan 12 22:53:18 2010 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Jan 13 00:08:56 2010 +0100
     1.3 @@ -7,10 +7,6 @@
     1.4  
     1.5  (* First some functions that should be in the library *)
     1.6  
     1.7 -(* A tactic which only succeeds when the argument *)
     1.8 -(* tactic solves completely the specified subgoal *)
     1.9 -fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
    1.10 -
    1.11  fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
    1.12    let
    1.13      val thy = theory_of_thm st;
    1.14 @@ -165,10 +161,10 @@
    1.15      val post_rewrite_tacs =
    1.16            [rtac pt_name_inst,
    1.17             rtac at_name_inst,
    1.18 -           TRY o SOLVEI (NominalPermeq.finite_guess_tac ss''),
    1.19 +           TRY o SOLVED' (NominalPermeq.finite_guess_tac ss''),
    1.20             inst_fresh vars params THEN'
    1.21 -           (TRY o SOLVEI (NominalPermeq.fresh_guess_tac ss'')) THEN'
    1.22 -           (TRY o SOLVEI (asm_full_simp_tac ss''))]
    1.23 +           (TRY o SOLVED' (NominalPermeq.fresh_guess_tac ss'')) THEN'
    1.24 +           (TRY o SOLVED' (asm_full_simp_tac ss''))]
    1.25    in
    1.26     ((if no_asm then no_tac else
    1.27      (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i)))