# HG changeset patch
# User narboux
# Date 1175710952 -7200
# Node ID 293934e41dfd48b607da56d1c4342f9e2aa4ff69
# Parent  33a690455f88a9e0158635a6cffd8c1de066b08c
make fresh_guess fail if it does not solve the subgoal

diff -r 33a690455f88 -r 293934e41dfd src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Wed Apr 04 19:56:25 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Apr 04 20:22:32 2007 +0200
@@ -78,6 +78,9 @@
 (* needed to avoid warnings about overwritten congs *)
 val weak_congs   = [thm "if_weak_cong"]
 
+(* a tactical which fails if the tactic taken as an argument generates does not solve the sub goal i *)
+
+fun SOLVEI t = t THEN_ALL_NEW (fn i => no_tac);
 
 (* debugging *)
 fun DEBUG_tac (msg,tac) = 
@@ -313,6 +316,7 @@
     end
     handle Subscript => Seq.empty
 
+
 (* tactic that guesses whether an atom is fresh for an expression  *)
 (* it first collects all free variables and tries to show that the *) 
 (* support of these free variables (op supports) the goal          *)
@@ -355,18 +359,18 @@
     end
     handle Subscript => Seq.empty;
 
-
 (* setup so that the simpset is used which is active at the moment when the tactic is called *)
 fun local_simp_meth_setup tac =
   Method.only_sectioned_args (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
   (Method.SIMPLE_METHOD' o tac o local_simpset_of) ;
 
-(* uses HOL_basic_ss only *)
+(* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
+
 fun basic_simp_meth_setup tac =
   Method.sectioned_args 
    (fn (ctxt,l) => ((),((Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt),l)))
    (Simplifier.simp_modifiers' @ Splitter.split_modifiers)
-   (fn _ => Method.SIMPLE_METHOD' o tac o local_simpset_of);
+   (fn _ => Method.SIMPLE_METHOD' o (fn ss => SOLVEI (tac ss)) o local_simpset_of);
 
 
 val perm_simp_meth            = local_simp_meth_setup (perm_simp_tac NO_DEBUG_tac);