# HG changeset patch
# User wenzelm
# Date 1130531271 -7200
# Node ID 853e8219732a7bbe95df78e0533711ef58e24fcc
# Parent  3900037edf3d94be26b5479a5e8b50fab61e1688
renamed Goal constant to prop;

diff -r 3900037edf3d -r 853e8219732a src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Fri Oct 28 22:27:47 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Fri Oct 28 22:27:51 2005 +0200
@@ -233,7 +233,7 @@
       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
       
 val has_meta_conn = 
-    exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "Goal"]);
+    exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
   
 (*Raises an exception if any Vars in the theorem mention type bool; they
   could cause make_horn to loop! Also rejects functions whose arguments are 
diff -r 3900037edf3d -r 853e8219732a src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 28 22:27:47 2005 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Oct 28 22:27:51 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.goalD", _), _, _, _) % _ %%
-        (PThm (("ProtoPure.goalI", _), _, _, _) % _ %% prf)) = SOME prf
+    fun rew' _ (PThm (("ProtoPure.protectD", _), _, _, _) % _ %%
+        (PThm (("ProtoPure.protectI", _), _, _, _) % _ %% prf)) = SOME prf
       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
         (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
       | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
@@ -41,16 +41,16 @@
             SOME (equal_intr_axm % B % A %% prf2 %% prf1)
 
       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
-        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("Goal", _)) %
+        (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm (("ProtoPure.goalI", _), _, _, _)) % _ %% prf2)) =
+        ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% 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.combination", _, _) % SOME (Const ("prop", _)) %
              _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm (("ProtoPure.goalI", _), _, _, _)) % _ %% prf2)) =
+        ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
 
diff -r 3900037edf3d -r 853e8219732a src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Oct 28 22:27:47 2005 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Oct 28 22:27:51 2005 +0200
@@ -251,7 +251,7 @@
   ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000))];
 
 val pure_syntax_output =
- [("Goal", "prop => prop", Mixfix ("_", [0], 0)),
+ [("prop", "prop => prop", Mixfix ("_", [0], 0)),
   ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))];
 
 val pure_appl_syntax =