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/datatype_simprocs.ML
changeset 78801 42ae6e0ecfd4
parent 78800 0b3700d31758 
--- a/src/HOL/Tools/datatype_simprocs.ML	Thu Oct 19 17:06:39 2023 +0200
+++ b/src/HOL/Tools/datatype_simprocs.ML	Thu Oct 19 21:38:09 2023 +0200
@@ -6,7 +6,7 @@
 *)
 
 signature DATATYPE_SIMPROCS = sig
-  val no_proper_subterm_simproc : Simplifier.proc
+  val no_proper_subterm_proc : Simplifier.proc
 end
 
 structure Datatype_Simprocs : DATATYPE_SIMPROCS = struct
@@ -86,7 +86,7 @@
    - support for nested datatypes
    - replace size-based proof with proper subexpression relation
 *)
-fun no_proper_subterm_simproc ctxt ct =
+fun no_proper_subterm_proc ctxt ct =
   let
     val (clhs, crhs) = ct |> Thm.dest_comb |> apfst (Thm.dest_comb #> snd)
     val (lhs, rhs) = apply2 Thm.term_of (clhs, crhs)
isabelle