changeset 42795 | 66fcc9882784 |
parent 42793 | 88bee9f6eec7 |
child 51717 | 9e7d1c139569 |
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 23:24:06 2011 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Fri May 13 23:58:40 2011 +0200 @@ -338,7 +338,7 @@ fun decomp_scnp_tac orders ctxt = let val extra_simps = Function_Common.Termination_Simps.get ctxt - val autom_tac = auto_tac (map_simpset_local (fn ss => ss addsimps extra_simps) ctxt) + val autom_tac = auto_tac (map_simpset (fn ss => ss addsimps extra_simps) ctxt) in gen_sizechange_tac orders autom_tac ctxt end