# HG changeset patch
# User narboux
# Date 1176449015 -7200
# Node ID 13302b2d09485d257506570a94eed25624cc1d4c
# Parent  83878e551c8cbf40d5f7e528bed8a1360e708354
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal

diff -r 83878e551c8c -r 13302b2d0948 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Fri Apr 13 01:06:12 2007 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML	Fri Apr 13 09:23:35 2007 +0200
@@ -375,11 +375,11 @@
 
 (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
 
-fun basic_simp_meth_setup tac =
+fun basic_simp_meth_setup debug 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 (fn ss => SOLVEI (tac ss)) o local_simpset_of);
+   (fn _ => Method.SIMPLE_METHOD' o (fn ss => if debug then (tac ss) else SOLVEI (tac ss)) o local_simpset_of);
 
 
 val perm_simp_meth            = local_simp_meth_setup (perm_simp_tac NO_DEBUG_tac);
@@ -388,10 +388,10 @@
 val perm_full_simp_meth_debug = local_simp_meth_setup (perm_full_simp_tac DEBUG_tac);
 val supports_meth             = local_simp_meth_setup (supports_tac NO_DEBUG_tac);
 val supports_meth_debug       = local_simp_meth_setup (supports_tac DEBUG_tac);
-val finite_guess_meth         = basic_simp_meth_setup (finite_guess_tac NO_DEBUG_tac);
-val finite_guess_meth_debug   = basic_simp_meth_setup (finite_guess_tac DEBUG_tac);
-val fresh_guess_meth          = basic_simp_meth_setup (fresh_guess_tac NO_DEBUG_tac);
-val fresh_guess_meth_debug    = basic_simp_meth_setup (fresh_guess_tac DEBUG_tac);
+val finite_guess_meth         = basic_simp_meth_setup false (finite_guess_tac NO_DEBUG_tac);
+val finite_guess_meth_debug   = basic_simp_meth_setup true (finite_guess_tac DEBUG_tac);
+val fresh_guess_meth          = basic_simp_meth_setup false (fresh_guess_tac NO_DEBUG_tac);
+val fresh_guess_meth_debug    = basic_simp_meth_setup true (fresh_guess_tac DEBUG_tac);
 
 val perm_simp_tac = perm_simp_tac NO_DEBUG_tac;
 val perm_full_simp_tac = perm_full_simp_tac NO_DEBUG_tac;