src/Pure/Proof/proof_rewrite_rules.ML

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jun 28 19:51:19 2002 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Jun 28 19:51:40 2002 +0200
@@ -27,7 +27,7 @@
       if b then PAxm (s, prop, Some Ts) else prf;
     fun ty T = if b then
         let val Type (_, [Type (_, [U, _]), _]) = T
-        in Some T end
+        in Some U end
       else None;
     val equal_intr_axm = ax equal_intr_axm [];
     val equal_elim_axm = ax equal_elim_axm [];
@@ -169,6 +169,15 @@
             (equal_elim_axm %> D %> B %% (symmetric_axm % ? B % ? D %% prf3) %%
               (equal_elim_axm %> C %> D %% prf2 %% prf4)))
 
+      | rew' _ ((prf as PAxm ("ProtoPure.combination", _, _) %
+        Some ((eq as Const ("==", T)) $ t) % _ % _ % _) %%
+          (PAxm ("ProtoPure.reflexive", _, _) % _)) =
+        let val (U, V) = (case T of
+          Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
+        in Some (prf %% (ax combination_axm [V, U] %> eq % ? eq % ? t % ? t %%
+          (ax reflexive_axm [T] % ? eq) %% (ax reflexive_axm [U] % ? t)))
+        end
+
       | rew' _ _ = None;
   in rew' end;