# HG changeset patch
# User wenzelm
# Date 976725813 -3600
# Node ID 75a1c9575edb8bdd35fb5eff988c0e15372ceb6b
# Parent  d2a7c5be62be30a4be883de11846dd8d22e10655
eliminated GOAL syntax;

diff -r d2a7c5be62be -r 75a1c9575edb src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Dec 13 17:41:10 2000 +0100
+++ b/src/Pure/drule.ML	Wed Dec 13 17:43:33 2000 +0100
@@ -703,17 +703,18 @@
     flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
 
 
-(*** GOAL (PROP A) <==> PROP A ***)
+(*** Goal (PROP A) <==> PROP A ***)
 
 local
-  val A = read_prop "PROP A";
-  val G = read_prop "GOAL (PROP A)";
+  val cert = Thm.cterm_of proto_sign;
+  val A = Free ("A", propT);
+  val G = Logic.mk_goal A;
   val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
 in
-  val triv_goal = store_thm "triv_goal"
-    (tag_rule internal_tag (standard (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A))));
-  val rev_triv_goal = store_thm "rev_triv_goal"
-    (tag_rule internal_tag (standard (Thm.equal_elim G_def (Thm.assume G))));
+  val triv_goal = store_thm "triv_goal" (tag_rule internal_tag (standard
+      (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume (cert A)))));
+  val rev_triv_goal = store_thm "rev_triv_goal" (tag_rule internal_tag (standard
+      (Thm.equal_elim G_def (Thm.assume (cert G)))));
 end;
 
 val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const);
diff -r d2a7c5be62be -r 75a1c9575edb src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Dec 13 17:41:10 2000 +0100
+++ b/src/Pure/pure_thy.ML	Wed Dec 13 17:43:33 2000 +0100
@@ -137,7 +137,7 @@
     val ref {space, thms_tab, ...} = get_theorems thy;
   in
     fn name =>
-      apsome (map (Thm.transfer_sg (Sign.deref sg_ref)))  	(*semi-dynamic identity*)
+      apsome (map (Thm.transfer_sg (Sign.deref sg_ref)))        (*semi-dynamic identity*)
       (Symtab.lookup (thms_tab, NameSpace.intern space name))   (*static content*)
   end;
 
@@ -474,7 +474,7 @@
     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
-    ("Goal", "prop => prop", Mixfix ("GOAL _", [1000], 999)),
+    ("Goal", "prop => prop", NoSyn),
     ("TYPE", "'a itself", NoSyn),
     (Term.dummy_patternN, "'a", Delimfix "'_")]
   |> Theory.add_modesyntax ("", false)
@@ -482,8 +482,9 @@
       :: Syntax.pure_appl_syntax)
   |> local_path
   |> (#1 oo (add_defs false o map Thm.no_attributes))
-   [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
-    ("Goal_def", "GOAL (PROP A) == PROP A")]
+   [("flexpair_def", "(t =?= u) == (t == u::'a::{})")]
+  |> (#1 oo (add_defs_i false o map Thm.no_attributes))
+   [("Goal_def", let val A = Free ("A", propT) in Logic.mk_equals (Logic.mk_goal A, A) end)]
   |> (#1 o add_thmss [(("nothing", []), [])])
   |> end_theory;