src/HOL/Nominal/nominal_fresh_fun.ML

            TRY' (SOLVEI (NominalPermeq.finite_guess_tac ss'')),
            inst_fresh vars params THEN'
            (TRY' (SOLVEI (NominalPermeq.fresh_guess_tac ss''))) THEN'
            (TRY' (SOLVEI (asm_full_simp_tac ss'')))] 
   in 
-   ((if no_asm then 
-    (subst_inner_asm_tac ctx fresh_fun_app' i THENL post_rewrite_tacs)
-    else 
-     no_tac) 
+   ((if no_asm then no_tac else
+    (subst_inner_asm_tac ctx fresh_fun_app' i THENL post_rewrite_tacs)) 
     ORELSE
     (subst_inner_tac     ctx fresh_fun_app' i THENL post_rewrite_tacs)) st
   end)) thm
   
   end