# HG changeset patch
# User narboux
# Date 1180008246 -7200
# Node ID f1df8d2da98adc986a1fe517eb59b14c78151ee8
# Parent  e3735771e7ba88e6c09452e4e724b44a33468e6a
fix a bug : the semantics of no_asm was the opposite

diff -r e3735771e7ba -r f1df8d2da98a src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu May 24 13:59:54 2007 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu May 24 14:04:06 2007 +0200
@@ -184,10 +184,8 @@
            (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