src/Pure/Proof/proof_rewrite_rules.ML

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Thu Jul 25 14:01:06 2019 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jul 26 09:35:02 2019 +0200
@@ -35,12 +35,12 @@
     val equal_elim_axm = ax Proofterm.equal_elim_axm [];
     val symmetric_axm = ax Proofterm.symmetric_axm [propT];
 
-    fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %%
-        (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
-      | rew' (PThm (_, (("Pure.conjunctionD1", _, _), _)) % _ % _ %%
-        (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PThm (_, (("Pure.conjunctionD2", _, _), _)) % _ % _ %%
-        (PThm (_, (("Pure.conjunctionI", _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
+    fun rew' (PThm (_, (("Pure.protectD", _, _, _), _)) % _ %%
+        (PThm (_, (("Pure.protectI", _, _, _), _)) % _ %% prf)) = SOME prf
+      | rew' (PThm (_, (("Pure.conjunctionD1", _, _, _), _)) % _ % _ %%
+        (PThm (_, (("Pure.conjunctionI", _, _, _), _)) % _ % _ %% prf %% _)) = SOME prf
+      | rew' (PThm (_, (("Pure.conjunctionD2", _, _, _), _)) % _ % _ %%
+        (PThm (_, (("Pure.conjunctionI", _, _, _), _)) % _ % _ %% _ %% prf)) = SOME prf
       | rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
         (PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
       | rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
@@ -50,14 +50,14 @@
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
           _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
+        ((tg as PThm (_, (("Pure.protectI", _, _, _), _))) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
       | rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("Pure.symmetric", _, _) % _ % _ %%
           (PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
              _ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm (_, (("Pure.protectI", _, _), _))) % _ %% prf2)) =
+        ((tg as PThm (_, (("Pure.protectI", _, _, _), _))) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
 
@@ -233,7 +233,7 @@
       (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
   | insert_refl defs Ts prf =
       (case Proofterm.strip_combt prf of
-        (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
+        (PThm (_, ((s, prop, SOME Ts, _), _)), ts) =>
           if member (op =) defs s then
             let
               val vs = vars_of prop;
@@ -259,7 +259,7 @@
       let
         val cnames = map (fst o dest_Const o fst) defs';
         val thms = Proofterm.fold_proof_atoms true
-          (fn PThm (_, ((name, prop, _), _)) =>
+          (fn PThm (_, ((name, prop, _, _), _)) =>
               if member (op =) defnames name orelse
                 not (exists_Const (member (op =) cnames o #1) prop)
               then I