src/Pure/drule.ML
changeset 10667 75a1c9575edb
parent 10515 8430c8fa8a9f
child 10767 8fa4aafa7314
     1.1 --- a/src/Pure/drule.ML	Wed Dec 13 17:41:10 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Dec 13 17:43:33 2000 +0100
     1.3 @@ -703,17 +703,18 @@
     1.4      flexpair_intr o equal_abs_elim_list cts o flexpair_elim;
     1.5  
     1.6  
     1.7 -(*** GOAL (PROP A) <==> PROP A ***)
     1.8 +(*** Goal (PROP A) <==> PROP A ***)
     1.9  
    1.10  local
    1.11 -  val A = read_prop "PROP A";
    1.12 -  val G = read_prop "GOAL (PROP A)";
    1.13 +  val cert = Thm.cterm_of proto_sign;
    1.14 +  val A = Free ("A", propT);
    1.15 +  val G = Logic.mk_goal A;
    1.16    val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
    1.17  in
    1.18 -  val triv_goal = store_thm "triv_goal"
    1.19 -    (tag_rule internal_tag (standard (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume A))));
    1.20 -  val rev_triv_goal = store_thm "rev_triv_goal"
    1.21 -    (tag_rule internal_tag (standard (Thm.equal_elim G_def (Thm.assume G))));
    1.22 +  val triv_goal = store_thm "triv_goal" (tag_rule internal_tag (standard
    1.23 +      (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume (cert A)))));
    1.24 +  val rev_triv_goal = store_thm "rev_triv_goal" (tag_rule internal_tag (standard
    1.25 +      (Thm.equal_elim G_def (Thm.assume (cert G)))));
    1.26  end;
    1.27  
    1.28  val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const);