--- 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
--- 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),
--- 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));
--- 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);
--- 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);
--- 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 |>
--- 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);
--- 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
--- 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);