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/rewrite_hol_proof.ML
changeset 80295 8a9588ffc133
parent 79441 eb142693255f 
--- a/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jun 07 15:20:01 2024 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Fri Jun 07 23:53:31 2024 +0200
@@ -305,9 +305,9 @@
 
 (** Replace congruence rules by substitution rules **)
 
-fun strip_cong ps (PThm ({name = "HOL.cong", ...}, _) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm ({thm_name = ("HOL.cong", 0), ...}, _) % _ % _ % SOME x % SOME y %%
       prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
-  | strip_cong ps (PThm ({name = "HOL.refl", ...}, _) % SOME f %% _) = SOME (f, ps)
+  | strip_cong ps (PThm ({thm_name = ("HOL.refl", 0), ...}, _) % SOME f %% _) = SOME (f, ps)
   | strip_cong _ _ = NONE;
 
 val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst});
@@ -330,15 +330,15 @@
 
 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
 
-fun elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
-  | elim_cong_aux Ts (PThm ({name = "HOL.iffD1", ...}, _) % P % _ %% prf) =
+  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % P % _ %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
         (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
-  | elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % _ %% prf1 %% prf2) =
+  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 [] o
         apsnd (map (make_sym Ts))) (strip_cong [] prf1)
-  | elim_cong_aux Ts (PThm ({name = "HOL.iffD2", ...}, _) % _ % P %% prf) =
+  | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % P %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
         apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
   | elim_cong_aux _ _ = NONE;
isabelle