# HG changeset patch
# User wenzelm
# Date 1129911299 -7200
# Node ID 09485bdd4b6f2fd93f91b877790bd47d3859db61
# Parent  b48885914c1dd29915b960155b2f266c80fa19d1
renamed triv_goal to goalI, rev_triv_goal to goalD;

diff -r b48885914c1d -r 09485bdd4b6f src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 21 18:14:58 2005 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 21 18:14:59 2005 +0200
@@ -32,8 +32,8 @@
     val equal_elim_axm = ax equal_elim_axm [];
     val symmetric_axm = ax symmetric_axm [propT];
 
-    fun rew' _ (PThm (("ProtoPure.rev_triv_goal", _), _, _, _) % _ %%
-        (PThm (("ProtoPure.triv_goal", _), _, _, _) % _ %% prf)) = SOME prf
+    fun rew' _ (PThm (("ProtoPure.goalD", _), _, _, _) % _ %%
+        (PThm (("ProtoPure.goalI", _), _, _, _) % _ %% prf)) = SOME prf
       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
         (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
       | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
@@ -43,14 +43,14 @@
       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
+        ((tg as PThm (("ProtoPure.goalI", _), _, _, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
           (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
              _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
+        ((tg as PThm (("ProtoPure.goalI", _), _, _, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))