search bottom up to get the inner fresh fun
authornarboux
Mon May 21 19:14:12 2007 +0200 (2007-05-21)
changeset 23065ab28e8398670
parent 23064 6ee131d1a618
child 23066 26a9157b620a
search bottom up to get the inner fresh fun
src/HOL/Nominal/nominal_fresh_fun.ML
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 21 19:13:38 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon May 21 19:14:12 2007 +0200
     1.3 @@ -121,10 +121,10 @@
     1.4    | SOME atom_name  => generate_fresh_tac atom_name i thm               
     1.5    end
     1.6  
     1.7 -(* A substitution tactic, FIXME : change the search function to get the inner occurence of fresh_fun (bottom -> up search ) *)
     1.8 +(* A substitution tactic *)
     1.9  
    1.10 -val search_fun     = curry (Seq.flat o (uncurry EqSubst.searchf_lr_unify_valid));
    1.11 -val search_fun_asm = EqSubst.skip_first_asm_occs_search EqSubst.searchf_lr_unify_valid;
    1.12 +val search_fun     = curry (Seq.flat o (uncurry EqSubst.searchf_bt_unify_valid));
    1.13 +val search_fun_asm = EqSubst.skip_first_asm_occs_search EqSubst.searchf_bt_unify_valid;
    1.14  
    1.15  fun subst_outer_tac           ctx = EqSubst.eqsubst_tac' ctx search_fun;
    1.16  fun subst_outer_asm_tac_aux i ctx = EqSubst.eqsubst_asm_tac' ctx search_fun_asm i;