Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix a bug : the semantics of no_asm was the opposite
authornarboux
Thu, 24 May 2007 14:04:06 +0200
changeset 23094 f1df8d2da98a
parent 23093 e3735771e7ba
child 23095 45f10b70e891
fix a bug : the semantics of no_asm was the opposite
src/HOL/Nominal/nominal_fresh_fun.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle