Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/scnp_reconstruct.ML
changeset 57959 1bfed12a7646
parent 55642 63beb38e9258
child 58819 aa43c6f05bca 
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Sat Aug 16 19:01:31 2014 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Sat Aug 16 19:20:11 2014 +0200
@@ -331,7 +331,7 @@
 
 fun decomp_scnp_tac orders ctxt =
   let
-    val extra_simps = Function_Common.Termination_Simps.get ctxt
+    val extra_simps = Named_Theorems.get ctxt @{named_theorems termination_simp}
     val autom_tac = auto_tac (ctxt addsimps extra_simps)
   in
      gen_sizechange_tac orders autom_tac ctxt
isabelle