changeset 31902 | 862ae16a799d |
parent 31775 | 2b04504fcb69 |
child 32149 | ef59550a55d3 |
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 02 17:33:36 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 02 17:34:14 2009 +0200 @@ -405,7 +405,7 @@ fun decomp_scnp orders ctxt = let - val extra_simps = FundefCommon.TerminationSimps.get ctxt + val extra_simps = FundefCommon.Termination_Simps.get ctxt val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps) in SIMPLE_METHOD