# HG changeset patch
# User wenzelm
# Date 1129911284 -7200
# Node ID 6842ca6ecb871336e8a8cc5775473c699fa9c391
# Parent  5574f676092c2d906d981122aebfc09809234a57
renamed triv_goal to goalI, rev_triv_goal to goalD;
removed mk_triv_goal (cf. Goal.init);

diff -r 5574f676092c -r 6842ca6ecb87 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Oct 21 18:14:43 2005 +0200
+++ b/src/Pure/drule.ML	Fri Oct 21 18:14:44 2005 +0200
@@ -126,11 +126,10 @@
   val norm_hhf_eq: thm
   val is_norm_hhf: term -> bool
   val norm_hhf: theory -> term -> term
-  val triv_goal: thm
-  val rev_triv_goal: thm
+  val goalI: thm
+  val goalD: thm
   val implies_intr_goals: cterm list -> thm -> thm
   val freeze_all: thm -> thm
-  val mk_triv_goal: cterm -> thm
   val tvars_of_terms: term list -> (indexname * sort) list
   val vars_of_terms: term list -> (indexname * typ) list
   val tvars_of: thm -> (indexname * sort) list
@@ -929,21 +928,20 @@
   val G = Logic.mk_goal A;
   val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
 in
-  val triv_goal = store_thm "triv_goal" (kind_rule internalK (standard
+  val goalI = store_thm "goalI" (kind_rule internalK (standard
       (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume (cert A)))));
-  val rev_triv_goal = store_thm "rev_triv_goal" (kind_rule internalK (standard
+  val goalD = store_thm "goalD" (kind_rule internalK (standard
       (Thm.equal_elim G_def (Thm.assume (cert G)))));
 end;
 
 val mk_cgoal = Thm.capply (Thm.cterm_of ProtoPure.thy Logic.goal_const);
-fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal;
+fun assume_goal ct = Thm.assume (mk_cgoal ct) RS goalD;
 
 fun implies_intr_goals cprops thm =
   implies_elim_list (implies_intr_list cprops thm) (map assume_goal cprops)
   |> implies_intr_list (map mk_cgoal cprops);
 
 
-
 (** variations on instantiate **)
 
 (*shorthand for instantiating just one variable in the current theory*)
@@ -1091,12 +1089,6 @@
 val freeze_all = freeze_all_Vars o freeze_all_TVars;
 
 
-(* mk_triv_goal *)
-
-(*make an initial proof state, "PROP A ==> (PROP A)" *)
-fun mk_triv_goal ct = instantiate' [] [SOME ct] triv_goal;
-
-
 
 (** meta-level conjunction **)