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