# HG changeset patch
# User wenzelm
# Date 1131652631 -3600
# Node ID 6757627acf593817dcffbe682e5f15efe67ca17c
# Parent  4edcb5fdc3b063fb67ead8e80c6d04361cf70a7a
renamed Thm.cgoal_of to Thm.cprem_of;

diff -r 4edcb5fdc3b0 -r 6757627acf59 NEWS
--- a/NEWS	Thu Nov 10 17:33:14 2005 +0100
+++ b/NEWS	Thu Nov 10 20:57:11 2005 +0100
@@ -107,7 +107,7 @@
 Note that fold_index starts counting at index 0, not 1 like foldln used to.
 
 * Pure: primitive rule lift_rule now takes goal cterm instead of an
-actual goal state (thm).  Use Thm.lift_rule (Thm.cgoal_of st i) to
+actual goal state (thm).  Use Thm.lift_rule (Thm.cprem_of st i) to
 achieve the old behaviour.
 
 * Pure: the "Goal" constant is now called "prop", supporting a
diff -r 4edcb5fdc3b0 -r 6757627acf59 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Thu Nov 10 17:33:14 2005 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Thu Nov 10 20:57:11 2005 +0100
@@ -115,7 +115,7 @@
   (List.nth (prems_of st, i - 1)) of
     _ $ (_ $ (f $ x) $ (g $ y)) =>
       let
-        val cong' = Thm.lift_rule (Thm.cgoal_of st i) cong;
+        val cong' = Thm.lift_rule (Thm.cprem_of st i) cong;
         val _ $ (_ $ (f' $ x') $ (g' $ y')) =
           Logic.strip_assums_concl (prop_of cong');
         val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
@@ -155,7 +155,7 @@
     val prem = List.nth (prems_of state, i - 1);
     val params = Logic.strip_params prem;
     val (_, Type (tname, _)) = hd (rev params);
-    val exhaustion = Thm.lift_rule (Thm.cgoal_of state i) (exh_thm_of tname);
+    val exhaustion = Thm.lift_rule (Thm.cprem_of state i) (exh_thm_of tname);
     val prem' = hd (prems_of exhaustion);
     val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
     val exhaustion' = cterm_instantiate [(cterm_of sg (head_of lhs),
diff -r 4edcb5fdc3b0 -r 6757627acf59 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Nov 10 17:33:14 2005 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Nov 10 20:57:11 2005 +0100
@@ -1234,7 +1234,7 @@
     val g = nth (prems_of st) (i - 1);
     val params = Logic.strip_params g;
     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
-    val rule' = Thm.lift_rule (Thm.cgoal_of st i) rule;
+    val rule' = Thm.lift_rule (Thm.cprem_of st i) rule;
     val (P, ys) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_assums_concl (prop_of rule')));
     (* ca indicates if rule is a case analysis or induction rule *)
@@ -1260,7 +1260,7 @@
     val sg = sign_of_thm st;
     val g = nth (prems_of st) (i - 1);
     val params = Logic.strip_params g;
-    val exI' = Thm.lift_rule (Thm.cgoal_of st i) exI;
+    val exI' = Thm.lift_rule (Thm.cprem_of st i) exI;
     val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI'));
     val cx = cterm_of sg (fst (strip_comb x));
 
diff -r 4edcb5fdc3b0 -r 6757627acf59 src/HOLCF/adm_tac.ML
--- a/src/HOLCF/adm_tac.ML	Thu Nov 10 17:33:14 2005 +0100
+++ b/src/HOLCF/adm_tac.ML	Thu Nov 10 20:57:11 2005 +0100
@@ -113,7 +113,7 @@
   let val {sign, maxidx, ...} = rep_thm state;
       val j = maxidx+1;
       val parTs = map snd (rev params);
-      val rule = Thm.lift_rule (Thm.cgoal_of state i) adm_subst;
+      val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst;
       val types = valOf o (fst (types_sorts rule));
       val tT = types ("t", j);
       val PT = types ("P", j);
diff -r 4edcb5fdc3b0 -r 6757627acf59 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Thu Nov 10 17:33:14 2005 +0100
+++ b/src/Provers/splitter.ML	Thu Nov 10 20:57:11 2005 +0100
@@ -302,7 +302,7 @@
 
 fun inst_split Ts t tt thm TB state i =
   let
-    val thm' = Thm.lift_rule (Thm.cgoal_of state i) thm;
+    val thm' = Thm.lift_rule (Thm.cprem_of state i) thm;
     val (P, _) = strip_comb (fst (Logic.dest_equals
       (Logic.strip_assums_concl (#prop (rep_thm thm')))));
     val cert = cterm_of (sign_of_thm state);
diff -r 4edcb5fdc3b0 -r 6757627acf59 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Nov 10 17:33:14 2005 +0100
+++ b/src/Pure/Isar/method.ML	Thu Nov 10 20:57:11 2005 +0100
@@ -435,7 +435,7 @@
         val lifttvar = pairself (ctyp_of thy o Logic.incr_tvar inc);
         val rule = Drule.instantiate
               (map lifttvar envT', map liftpair cenv)
-              (Thm.lift_rule (Thm.cgoal_of st i) thm)
+              (Thm.lift_rule (Thm.cprem_of st i) thm)
       in
         if i > nprems_of st then no_tac st
         else st |>
diff -r 4edcb5fdc3b0 -r 6757627acf59 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Thu Nov 10 17:33:14 2005 +0100
+++ b/src/Pure/goal.ML	Thu Nov 10 20:57:11 2005 +0100
@@ -84,7 +84,7 @@
 (* composition of normal results *)
 
 fun compose_hhf tha i thb =
-  Thm.bicompose false (false, Drule.lift_all (Thm.cgoal_of thb i) tha, 0) i thb;
+  Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of thb i) tha, 0) i thb;
 
 fun compose_hhf_tac th i = PRIMSEQ (compose_hhf th i);
 
@@ -161,7 +161,7 @@
   composing the resulting thm with the original state.*)
 
 fun SELECT tac i st =
-  init (Thm.adjust_maxidx (List.nth (Drule.cprems_of st, i - 1)))
+  init (Thm.adjust_maxidx (Thm.cprem_of st i))
   |> tac
   |> Seq.maps (fn st' => Thm.bicompose false (false, conclude st', Thm.nprems_of st') i st);
 
diff -r 4edcb5fdc3b0 -r 6757627acf59 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Thu Nov 10 17:33:14 2005 +0100
+++ b/src/Pure/tactic.ML	Thu Nov 10 20:57:11 2005 +0100
@@ -253,7 +253,7 @@
     fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
     val lifttvar = pairself (ctyp_fun (Logic.incr_tvar inc))
 in Drule.instantiate (map lifttvar Tinsts, map liftpair insts)
-                     (Thm.lift_rule (Thm.cgoal_of st i) rule)
+                     (Thm.lift_rule (Thm.cprem_of st i) rule)
 end;
 
 fun lift_inst_rule (st, i, sinsts, rule) = lift_inst_rule'
@@ -285,7 +285,7 @@
       (ctyp_of thy (TVar ((a, i + inc), S)),
        ctyp_of thy (Logic.incr_tvar inc T))
 in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
-                     (Thm.lift_rule (Thm.cgoal_of st i) rule)
+                     (Thm.lift_rule (Thm.cprem_of st i) rule)
 end;
 
 (*** Resolve after lifting and instantation; may refer to parameters of the
diff -r 4edcb5fdc3b0 -r 6757627acf59 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Nov 10 17:33:14 2005 +0100
+++ b/src/Pure/thm.ML	Thu Nov 10 20:57:11 2005 +0100
@@ -83,7 +83,7 @@
   val prems_of: thm -> term list
   val nprems_of: thm -> int
   val cprop_of: thm -> cterm
-  val cgoal_of: thm -> int -> cterm
+  val cprem_of: thm -> int -> cterm
   val transfer: theory -> thm -> thm
   val weaken: cterm -> thm -> thm
   val extra_shyps: thm -> sort list
@@ -451,9 +451,9 @@
 fun cprop_of (Thm {thy_ref, maxidx, shyps, prop, ...}) =
   Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop, sorts = shyps};
 
-fun cgoal_of (th as Thm {thy_ref, maxidx, shyps, prop, ...}) i =
+fun cprem_of (th as Thm {thy_ref, maxidx, shyps, prop, ...}) i =
   Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, sorts = shyps,
-    t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cgoal_of", i, [th])};
+    t = Logic.nth_prem (i, prop) handle TERM _ => raise THM ("cprem_of", i, [th])};
 
 (*explicit transfer to a super theory*)
 fun transfer thy' thm =
@@ -1472,7 +1472,7 @@
   Puts the rule above:  rule/state.  Renames vars in the rules. *)
 fun biresolution match brules i state =
     let val (stpairs, Bs, Bi, C) = dest_state(state,i);
-        val lift = lift_rule (cgoal_of state i);
+        val lift = lift_rule (cprem_of state i);
         val B = Logic.strip_assums_concl Bi;
         val Hs = Logic.strip_assums_hyp Bi;
         val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);