src/HOL/Nominal/nominal_fresh_fun.ML
changeset 23094 f1df8d2da98a
parent 23091 c91530f18d9c
child 23368 ad690b9bca1c
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu May 24 13:59:54 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu May 24 14:04:06 2007 +0200
     1.3 @@ -184,10 +184,8 @@
     1.4             (TRY' (SOLVEI (NominalPermeq.fresh_guess_tac ss''))) THEN'
     1.5             (TRY' (SOLVEI (asm_full_simp_tac ss'')))] 
     1.6    in 
     1.7 -   ((if no_asm then 
     1.8 -    (subst_inner_asm_tac ctx fresh_fun_app' i THENL post_rewrite_tacs)
     1.9 -    else 
    1.10 -     no_tac) 
    1.11 +   ((if no_asm then no_tac else
    1.12 +    (subst_inner_asm_tac ctx fresh_fun_app' i THENL post_rewrite_tacs)) 
    1.13      ORELSE
    1.14      (subst_inner_tac     ctx fresh_fun_app' i THENL post_rewrite_tacs)) st
    1.15    end)) thm