# HG changeset patch
# User narboux
# Date 1179767652 -7200
# Node ID ab28e839867074b015215581587eee499b37c7fb
# Parent  6ee131d1a618e9ac7897d1ba3bc53f711581e4aa
search bottom up to get the inner fresh fun

diff -r 6ee131d1a618 -r ab28e8398670 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 21 19:13:38 2007 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 21 19:14:12 2007 +0200
@@ -121,10 +121,10 @@
   | SOME atom_name  => generate_fresh_tac atom_name i thm               
   end
 
-(* A substitution tactic, FIXME : change the search function to get the inner occurence of fresh_fun (bottom -> up search ) *)
+(* A substitution tactic *)
 
-val search_fun     = curry (Seq.flat o (uncurry EqSubst.searchf_lr_unify_valid));
-val search_fun_asm = EqSubst.skip_first_asm_occs_search EqSubst.searchf_lr_unify_valid;
+val search_fun     = curry (Seq.flat o (uncurry EqSubst.searchf_bt_unify_valid));
+val search_fun_asm = EqSubst.skip_first_asm_occs_search EqSubst.searchf_bt_unify_valid;
 
 fun subst_outer_tac           ctx = EqSubst.eqsubst_tac' ctx search_fun;
 fun subst_outer_asm_tac_aux i ctx = EqSubst.eqsubst_asm_tac' ctx search_fun_asm i;