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/Pure/Proof/proof_rewrite_rules.ML
changeset 80635 27d5452d20fc
parent 80590 505f97165f52
child 81505 01f2936ec85e 
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Sun Aug 04 13:24:54 2024 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Sun Aug 04 16:56:28 2024 +0200
@@ -269,7 +269,7 @@
     val prf' =
       if r then
         let
-          val cnames = map (fst o dest_Const o fst) defs';
+          val cnames = map (dest_Const_name o fst) defs';
           val expand = Proofterm.fold_proof_atoms true
             (fn PThm ({serial, thm_name = (thm_name, _), prop, ...}, _) =>
                 if member (op =) defnames thm_name orelse
isabelle