--- a/TFL/dcterm.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/TFL/dcterm.ML Wed Apr 04 23:29:33 2007 +0200
@@ -187,9 +187,9 @@
*---------------------------------------------------------------------------*)
fun mk_prop ctm =
- let val {t, sign, ...} = Thm.rep_cterm ctm in
+ let val {t, thy, ...} = Thm.rep_cterm ctm in
if can HOLogic.dest_Trueprop t then ctm
- else Thm.cterm_of sign (HOLogic.mk_Trueprop t)
+ else Thm.cterm_of thy (HOLogic.mk_Trueprop t)
end
handle TYPE (msg, _, _) => raise ERR "mk_prop" msg
| TERM (msg, _) => raise ERR "mk_prop" msg;
--- a/TFL/post.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/TFL/post.ML Wed Apr 04 23:29:33 2007 +0200
@@ -105,8 +105,8 @@
fun rewrite L = rewrite_rule (map mk_meta_eq (List.filter(not o id_thm) L))
fun join_assums th =
- let val {sign,...} = rep_thm th
- val tych = cterm_of sign
+ let val {thy,...} = rep_thm th
+ val tych = cterm_of thy
val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *)
val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *)
--- a/TFL/rules.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/TFL/rules.ML Wed Apr 04 23:29:33 2007 +0200
@@ -171,17 +171,17 @@
(*----------------------------------------------------------------------------
* Disjunction
*---------------------------------------------------------------------------*)
-local val {prop,sign,...} = rep_thm disjI1
+local val {prop,thy,...} = rep_thm disjI1
val [P,Q] = term_vars prop
- val disj1 = Thm.forall_intr (Thm.cterm_of sign Q) disjI1
+ val disj1 = Thm.forall_intr (Thm.cterm_of thy Q) disjI1
in
fun DISJ1 thm tm = thm RS (forall_elim (D.drop_prop tm) disj1)
handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
end;
-local val {prop,sign,...} = rep_thm disjI2
+local val {prop,thy,...} = rep_thm disjI2
val [P,Q] = term_vars prop
- val disj2 = Thm.forall_intr (Thm.cterm_of sign P) disjI2
+ val disj2 = Thm.forall_intr (Thm.cterm_of thy P) disjI2
in
fun DISJ2 tm thm = thm RS (forall_elim (D.drop_prop tm) disj2)
handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
@@ -274,14 +274,14 @@
* Universals
*---------------------------------------------------------------------------*)
local (* this is fragile *)
- val {prop,sign,...} = rep_thm spec
+ val {prop,thy,...} = rep_thm spec
val x = hd (tl (term_vars prop))
- val cTV = ctyp_of sign (type_of x)
- val gspec = forall_intr (cterm_of sign x) spec
+ val cTV = ctyp_of thy (type_of x)
+ val gspec = forall_intr (cterm_of thy x) spec
in
fun SPEC tm thm =
- let val {sign,T,...} = rep_cterm tm
- val gspec' = instantiate ([(cTV, ctyp_of sign T)], []) gspec
+ let val {thy,T,...} = rep_cterm tm
+ val gspec' = instantiate ([(cTV, ctyp_of thy T)], []) gspec
in
thm RS (forall_elim tm gspec')
end
@@ -293,7 +293,7 @@
val ISPECL = fold ISPEC;
(* Not optimized! Too complicated. *)
-local val {prop,sign,...} = rep_thm allI
+local val {prop,thy,...} = rep_thm allI
val [P] = add_term_vars (prop, [])
fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty))
fun ctm_theta s = map (fn (i, (_, tm2)) =>
@@ -306,22 +306,22 @@
in
fun GEN v th =
let val gth = forall_intr v th
- val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
+ val {prop=Const("all",_)$Abs(x,ty,rst),thy,...} = rep_thm gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
- val theta = Pattern.match sign (P,P') (Vartab.empty, Vartab.empty);
- val allI2 = instantiate (certify sign theta) allI
+ val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
+ val allI2 = instantiate (certify thy theta) allI
val thm = Thm.implies_elim allI2 gth
- val {prop = tp $ (A $ Abs(_,_,M)),sign,...} = rep_thm thm
+ val {prop = tp $ (A $ Abs(_,_,M)),thy,...} = rep_thm thm
val prop' = tp $ (A $ Abs(x,ty,M))
- in ALPHA thm (cterm_of sign prop')
+ in ALPHA thm (cterm_of thy prop')
end
end;
val GENL = fold_rev GEN;
fun GEN_ALL thm =
- let val {prop,sign,...} = rep_thm thm
- val tycheck = cterm_of sign
+ let val {prop,thy,...} = rep_thm thm
+ val tycheck = cterm_of thy
val vlist = map tycheck (add_term_vars (prop, []))
in GENL vlist thm
end;
@@ -352,20 +352,20 @@
let
val lam = #2 (D.dest_comb (D.drop_prop (cconcl exth)))
val redex = D.capply lam fvar
- val {sign, t = t$u,...} = Thm.rep_cterm redex
- val residue = Thm.cterm_of sign (Term.betapply (t, u))
+ val {thy, t = t$u,...} = Thm.rep_cterm redex
+ val residue = Thm.cterm_of thy (Term.betapply (t, u))
in
GEN fvar (DISCH residue fact) RS (exth RS Thms.choose_thm)
handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
end;
-local val {prop,sign,...} = rep_thm exI
+local val {prop,thy,...} = rep_thm exI
val [P,x] = term_vars prop
in
fun EXISTS (template,witness) thm =
- let val {prop,sign,...} = rep_thm thm
- val P' = cterm_of sign P
- val x' = cterm_of sign x
+ let val {prop,thy,...} = rep_thm thm
+ val P' = cterm_of thy P
+ val x' = cterm_of thy x
val abstr = #2 (D.dest_comb template)
in
thm RS (cterm_instantiate[(P',abstr), (x',witness)] exI)
@@ -396,11 +396,11 @@
(* Could be improved, but needs "subst_free" for certified terms *)
fun IT_EXISTS blist th =
- let val {sign,...} = rep_thm th
- val tych = cterm_of sign
+ let val {thy,...} = rep_thm th
+ val tych = cterm_of thy
val detype = #t o rep_cterm
val blist' = map (fn (x,y) => (detype x, detype y)) blist
- fun ex v M = cterm_of sign (S.mk_exists{Bvar=v,Body = M})
+ fun ex v M = cterm_of thy (S.mk_exists{Bvar=v,Body = M})
in
fold_rev (fn (b as (r1,r2)) => fn thm =>
@@ -413,8 +413,8 @@
(*---------------------------------------------------------------------------
* Faster version, that fails for some as yet unknown reason
* fun IT_EXISTS blist th =
- * let val {sign,...} = rep_thm th
- * val tych = cterm_of sign
+ * let val {thy,...} = rep_thm th
+ * val tych = cterm_of thy
* fun detype (x,y) = ((#t o rep_cterm) x, (#t o rep_cterm) y)
* in
* fold (fn (b as (r1,r2), thm) =>
@@ -521,8 +521,8 @@
(* Note: rename_params_rule counts from 1, not 0 *)
fun rename thm =
- let val {prop,sign,...} = rep_thm thm
- val tych = cterm_of sign
+ let val {prop,thy,...} = rep_thm thm
+ val tych = cterm_of thy
val ants = Logic.strip_imp_prems prop
val news = get (ants,1,[])
in
@@ -681,8 +681,8 @@
val dummy = thm_ref := (thm :: !thm_ref)
val dummy = ss_ref := (ss :: !ss_ref)
(* Unquantified eliminate *)
- fun uq_eliminate (thm,imp,sign) =
- let val tych = cterm_of sign
+ fun uq_eliminate (thm,imp,thy) =
+ let val tych = cterm_of thy
val dummy = print_cterms "To eliminate:" [tych imp]
val ants = map tych (Logic.strip_imp_prems imp)
val eq = Logic.strip_imp_concl imp
@@ -696,13 +696,13 @@
in
lhs_eeq_lhs2 COMP thm
end
- fun pq_eliminate (thm,sign,vlist,imp_body,lhs_eq) =
+ fun pq_eliminate (thm,thy,vlist,imp_body,lhs_eq) =
let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
val dummy = forall (op aconv) (ListPair.zip (vlist, args))
orelse error "assertion failed in CONTEXT_REWRITE_RULE"
val imp_body1 = subst_free (ListPair.zip (args, vstrl))
imp_body
- val tych = cterm_of sign
+ val tych = cterm_of thy
val ants1 = map tych (Logic.strip_imp_prems imp_body1)
val eq1 = Logic.strip_imp_concl imp_body1
val Q = get_lhs eq1
@@ -725,13 +725,13 @@
val ant_th = U.itlist2 (PGEN tych) args vstrl impth1
in ant_th COMP thm
end
- fun q_eliminate (thm,imp,sign) =
+ fun q_eliminate (thm,imp,thy) =
let val (vlist, imp_body, used') = strip_all used imp
val (ants,Q) = dest_impl imp_body
in if (pbeta_redex Q) (length vlist)
- then pq_eliminate (thm,sign,vlist,imp_body,Q)
+ then pq_eliminate (thm,thy,vlist,imp_body,Q)
else
- let val tych = cterm_of sign
+ let val tych = cterm_of thy
val ants1 = map tych ants
val ss' = MetaSimplifier.add_prems (map ASSUME ants1) ss
val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
@@ -746,11 +746,11 @@
fun eliminate thm =
case (rep_thm thm)
- of {prop = (Const("==>",_) $ imp $ _), sign, ...} =>
+ of {prop = (Const("==>",_) $ imp $ _), thy, ...} =>
eliminate
(if not(is_all imp)
- then uq_eliminate (thm,imp,sign)
- else q_eliminate (thm,imp,sign))
+ then uq_eliminate (thm,imp,thy)
+ else q_eliminate (thm,imp,thy))
(* Assume that the leading constant is ==, *)
| _ => thm (* if it is not a ==> *)
in SOME(eliminate (rename thm)) end
@@ -761,7 +761,7 @@
val cntxt = rev(MetaSimplifier.prems_of_ss ss)
val dummy = print_thms "cntxt:" cntxt
val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
- sign,...} = rep_thm thm
+ thy,...} = rep_thm thm
fun genl tm = let val vlist = subtract (op aconv) globals
(add_term_frees(tm,[]))
in fold_rev Forall vlist tm
@@ -781,15 +781,15 @@
val antl = case rcontext of [] => []
| _ => [S.list_mk_conj(map cncl rcontext)]
val TC = genl(S.list_mk_imp(antl, A))
- val dummy = print_cterms "func:" [cterm_of sign func]
+ val dummy = print_cterms "func:" [cterm_of thy func]
val dummy = print_cterms "TC:"
- [cterm_of sign (HOLogic.mk_Trueprop TC)]
+ [cterm_of thy (HOLogic.mk_Trueprop TC)]
val dummy = tc_list := (TC :: !tc_list)
val nestedp = isSome (S.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
val dummy = term_ref := ([func,TC]@(!term_ref))
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
- else let val cTC = cterm_of sign
+ else let val cTC = cterm_of thy
(HOLogic.mk_Trueprop TC)
in case rcontext of
[] => SPEC_ALL(ASSUME cTC)
--- a/src/FOLP/simp.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/FOLP/simp.ML Wed Apr 04 23:29:33 2007 +0200
@@ -381,12 +381,12 @@
(*print lhs of conclusion of subgoal i*)
fun pr_goal_lhs i st =
- writeln (Sign.string_of_term (#sign(rep_thm st))
+ writeln (Sign.string_of_term (Thm.theory_of_thm st)
(lhs_of (prepare_goal i st)));
(*print conclusion of subgoal i*)
fun pr_goal_concl i st =
- writeln (Sign.string_of_term (#sign(rep_thm st)) (prepare_goal i st))
+ writeln (Sign.string_of_term (Thm.theory_of_thm st) (prepare_goal i st))
(*print subgoals i to j (inclusive)*)
fun pr_goals (i,j) st =
@@ -431,7 +431,7 @@
are represented by rules, generalized over their parameters*)
fun add_asms(ss,thm,a,anet,ats,cs) =
let val As = strip_varify(nth_subgoal i thm, a, []);
- val thms = map (trivial o cterm_of(#sign(rep_thm(thm))))As;
+ val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
val new_rws = List.concat(map mk_rew_rules thms);
val rwrls = map mk_trans (List.concat(map mk_rew_rules thms));
val anet' = foldr lhs_insert_thm anet rwrls
--- a/src/HOL/Import/proof_kernel.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Apr 04 23:29:33 2007 +0200
@@ -194,9 +194,9 @@
fun simple_smart_string_of_cterm ct =
let
- val {sign,t,T,...} = rep_cterm ct
+ val {thy,t,T,...} = rep_cterm ct
(* Hack to avoid parse errors with Trueprop *)
- val ct = (cterm_of sign (HOLogic.dest_Trueprop t)
+ val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
handle TERM _ => ct)
in
quote(
@@ -212,9 +212,9 @@
fun smart_string_of_cterm ct =
let
- val {sign,t,T,...} = rep_cterm ct
+ val {thy,t,T,...} = rep_cterm ct
(* Hack to avoid parse errors with Trueprop *)
- val ct = (cterm_of sign (HOLogic.dest_Trueprop t)
+ val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
handle TERM _ => ct)
fun match cu = t aconv (term_of cu)
fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
@@ -225,7 +225,7 @@
fun F n =
let
val str = Library.setmp show_brackets false (G n string_of_cterm) ct
- val cu = read_cterm sign (str,T)
+ val cu = read_cterm thy (str,T)
in
if match cu
then quote str
--- a/src/HOL/Modelcheck/MuckeSyn.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML Wed Apr 04 23:29:33 2007 +0200
@@ -53,14 +53,14 @@
(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
REPEAT (resolve_tac prems 1)]);
- val sig_move_thm = #sign (rep_thm move_thm);
+ val sig_move_thm = Thm.theory_of_thm move_thm;
val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm))));
in
fun move_mus i state =
-let val sign = #sign (rep_thm state);
+let val sign = Thm.theory_of_thm state;
val (subgoal::_) = Library.drop(i-1,prems_of state);
val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
val redex = search_mu concl;
--- a/src/HOL/Modelcheck/mucke_oracle.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Wed Apr 04 23:29:33 2007 +0200
@@ -96,7 +96,7 @@
in
fun if_full_simp_tac sset i state =
-let val sign = #sign (rep_thm state);
+let val sign = Thm.theory_of_thm state;
val (subgoal::_) = Library.drop(i-1,prems_of state);
val prems = Logic.strip_imp_prems subgoal;
val concl = Logic.strip_imp_concl subgoal;
--- a/src/HOL/Tools/datatype_aux.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Wed Apr 04 23:29:33 2007 +0200
@@ -118,7 +118,7 @@
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
+ val insts = map (pairself (cterm_of (Thm.theory_of_thm st)) o
apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
in compose_tac (false, cterm_instantiate insts cong', 2) i st
--- a/src/HOL/Tools/datatype_realizer.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Wed Apr 04 23:29:33 2007 +0200
@@ -27,8 +27,8 @@
in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
fun prf_of thm =
- let val {sign, prop, der = (_, prf), ...} = rep_thm thm
- in Reconstruct.reconstruct_proof sign prop prf end;
+ let val {thy, prop, der = (_, prf), ...} = rep_thm thm
+ in Reconstruct.reconstruct_proof thy prop prf end;
fun prf_subst_vars inst =
Proofterm.map_proof_terms (subst_vars ([], inst)) I;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Apr 04 23:29:33 2007 +0200
@@ -356,7 +356,7 @@
fun mk_funs_inv thm =
let
- val {sign, prop, ...} = rep_thm thm;
+ val {thy, prop, ...} = rep_thm thm;
val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
(_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
val used = add_term_tfree_names (a, []);
@@ -366,7 +366,7 @@
val Ts = map (TFree o rpair HOLogic.typeS)
(Name.variant_list used (replicate i "'t"));
val f = Free ("f", Ts ---> U)
- in Goal.prove_global sign [] [] (Logic.mk_implies
+ in Goal.prove_global thy [] [] (Logic.mk_implies
(HOLogic.mk_Trueprop (HOLogic.list_all
(map (pair "x") Ts, S $ app_bnds f i)),
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
--- a/src/HOL/Tools/inductive_realizer.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Apr 04 23:29:33 2007 +0200
@@ -64,8 +64,8 @@
val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
fun prf_of thm =
- let val {sign, prop, der = (_, prf), ...} = rep_thm thm
- in Reconstruct.expand_proof sign [("", NONE)] (Reconstruct.reconstruct_proof sign prop prf) end; (* FIXME *)
+ let val {thy, prop, der = (_, prf), ...} = rep_thm thm
+ in Reconstruct.expand_proof thy [("", NONE)] (Reconstruct.reconstruct_proof thy prop prf) end; (* FIXME *)
fun forall_intr_prf (t, prf) =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
--- a/src/HOL/Tools/record_package.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Wed Apr 04 23:29:33 2007 +0200
@@ -1703,10 +1703,10 @@
fun meta_to_obj_all thm =
let
- val {sign, prop, ...} = rep_thm thm;
+ val {thy, prop, ...} = rep_thm thm;
val params = Logic.strip_params prop;
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
- val ct = cterm_of sign
+ val ct = cterm_of thy
(HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
in
--- a/src/HOL/Tools/res_axioms.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Apr 04 23:29:33 2007 +0200
@@ -394,10 +394,10 @@
let val (c,rhs) = Drule.dest_equals (cprop_of (freeze_thm def))
val (ch, frees) = c_variant_abs_multi (rhs, [])
val (chilbert,cabs) = Thm.dest_comb ch
- val {sign,t, ...} = rep_cterm chilbert
+ val {thy,t, ...} = rep_cterm chilbert
val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
| _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
- val cex = Thm.cterm_of sign (HOLogic.exists_const T)
+ val cex = Thm.cterm_of thy (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML Wed Apr 04 23:29:33 2007 +0200
@@ -3,9 +3,9 @@
(* call_sim_tac invokes oracle "Sim" *)
fun call_sim_tac thm_list i state =
-let val sign = #sign (rep_thm state);
+let val thy = Thm.theory_of_thm state;
val (subgoal::_) = Library.drop(i-1,prems_of state);
- val OraAss = sim_oracle sign (subgoal,thm_list);
+ val OraAss = sim_oracle thy (subgoal,thm_list);
in cut_facts_tac [OraAss] i state end;
--- a/src/HOLCF/adm_tac.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/HOLCF/adm_tac.ML Wed Apr 04 23:29:33 2007 +0200
@@ -110,7 +110,7 @@
(*** instantiation of adm_subst theorem (a bit tricky) ***)
fun inst_adm_subst_thm state i params s T subt t paths =
- let val {sign, maxidx, ...} = rep_thm state;
+ let val {thy = sign, maxidx, ...} = rep_thm state;
val j = maxidx+1;
val parTs = map snd (rev params);
val rule = Thm.lift_rule (Thm.cprem_of state i) adm_subst;
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Apr 04 23:29:33 2007 +0200
@@ -460,7 +460,7 @@
fun multn2(n,thm) =
let val SOME(mth) =
get_first (fn th => SOME(thm RS th) handle THM _ => NONE) mult_mono_thms
- fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var;
+ fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (Thm.theory_of_thm th) var;
val cv = cvar(mth, hd(prems_of mth));
val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
in instantiate ([],[(cv,ct)]) mth end
--- a/src/Provers/blast.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/Provers/blast.ML Wed Apr 04 23:29:33 2007 +0200
@@ -480,7 +480,7 @@
Flag "upd" says that the inference updated the branch.
Flag "dup" requests duplication of the affected formula.*)
fun fromRule vars rl =
- let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars
+ let val trl = rl |> Thm.prop_of |> fromTerm |> convertRule vars
fun tac (upd, dup,rot) i =
emtac upd (if dup then rev_dup_elim rl else rl) i
THEN
@@ -512,7 +512,7 @@
Since haz rules are now delayed, "dup" is always FALSE for
introduction rules.*)
fun fromIntrRule vars rl =
- let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars
+ let val trl = rl |> Thm.prop_of |> fromTerm |> convertIntrRule vars
fun tac (upd,dup,rot) i =
rmtac upd (if dup then Data.dup_intr rl else rl) i
THEN
@@ -1248,7 +1248,7 @@
"lim" is depth limit.*)
fun timing_depth_tac start cs lim i st0 =
let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0);
- val {sign,...} = rep_thm st
+ val sign = Thm.theory_of_thm st
val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
val hyps = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
@@ -1291,7 +1291,7 @@
(*Translate subgoal i from a proof state*)
fun trygl cs lim i =
let val st = topthm()
- val {sign,...} = rep_thm st
+ val sign = Thm.theory_of_thm st
val skoprem = (initialize (theory_of_thm st);
fromSubgoal (List.nth(prems_of st, i-1)))
val hyps = strip_imp_prems skoprem
--- a/src/Provers/splitter.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/Provers/splitter.ML Wed Apr 04 23:29:33 2007 +0200
@@ -293,7 +293,7 @@
*************************************************************)
fun select cmap state i =
- let val sg = #sign(rep_thm state)
+ let val sg = Thm.theory_of_thm state
val goali = nth_subgoal i state
val Ts = rev(map #2 (Logic.strip_params goali))
val _ $ t $ _ = Logic.strip_assums_concl goali;
@@ -323,7 +323,7 @@
fun inst_lift Ts t (T, U, pos) state i =
let
val cert = cterm_of (Thm.theory_of_thm state);
- val cntxt = mk_cntxt Ts t pos (T --> U) (#maxidx(rep_thm trlift));
+ val cntxt = mk_cntxt Ts t pos (T --> U) (Thm.maxidx_of trlift);
in cterm_instantiate [(cert P, cert cntxt)] trlift
end;
@@ -345,7 +345,7 @@
let
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')))));
+ (Logic.strip_assums_concl (Thm.prop_of thm'))));
val cert = cterm_of (Thm.theory_of_thm state);
val cntxt = mk_cntxt_splitthm t tt TB;
val abss = Library.foldl (fn (t, T) => Abs ("", T, t));
--- a/src/Pure/Proof/extraction.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/Pure/Proof/extraction.ML Wed Apr 04 23:29:33 2007 +0200
@@ -718,12 +718,12 @@
fun prep_thm (thm, vs) =
let
- val {prop, der = (_, prf), sign, ...} = rep_thm thm;
+ val {prop, der = (_, prf), thy, ...} = rep_thm thm;
val name = Thm.get_name thm;
val _ = name <> "" orelse error "extraction: unnamed theorem";
val _ = etype_of thy' vs [] prop <> nullT orelse error ("theorem " ^
quote name ^ " has no computational content")
- in (Reconstruct.reconstruct_proof sign prop prf, vs) end;
+ in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
val defs = Library.foldl (fn (defs, (prf, vs)) =>
fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
--- a/src/Pure/codegen.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/Pure/codegen.ML Wed Apr 04 23:29:33 2007 +0200
@@ -1064,8 +1064,8 @@
Logic.mk_equals (t, eval_term thy t);
fun evaluation_conv ct =
- let val {sign, t, ...} = rep_cterm ct
- in Thm.invoke_oracle_i sign "Pure.evaluation" (sign, Evaluation t) end;
+ let val {thy, t, ...} = rep_cterm ct
+ in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
val _ = Context.add_setup
(Theory.add_oracle ("evaluation", evaluation_oracle));
--- a/src/Pure/tctical.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/Pure/tctical.ML Wed Apr 04 23:29:33 2007 +0200
@@ -422,7 +422,7 @@
fun metahyps_aux_tac tacf (prem,gno) state =
let val (insts,params,hyps,concl) = metahyps_split_prem prem
- val {sign,maxidx,...} = rep_thm state
+ val {thy = sign,maxidx,...} = rep_thm state
val cterm = cterm_of sign
val chyps = map cterm hyps
val hypths = map assume chyps
@@ -451,7 +451,7 @@
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths
(*A form of lifting that discharges assumptions.*)
fun relift st =
- let val prop = #prop(rep_thm st)
+ let val prop = Thm.prop_of st
val subgoal_vars = (*Vars introduced in the subgoals*)
foldr add_term_vars [] (Logic.strip_imp_prems prop)
and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
@@ -477,7 +477,7 @@
fun metahyps_thms i state =
let val prem = Logic.nth_prem (i, Thm.prop_of state)
val (insts,params,hyps,concl) = metahyps_split_prem prem
- val cterm = cterm_of (#sign (rep_thm state))
+ val cterm = cterm_of (Thm.theory_of_thm state)
in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end
handle TERM ("nth_prem", [A]) => NONE;
--- a/src/Pure/thm.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/Pure/thm.ML Wed Apr 04 23:29:33 2007 +0200
@@ -13,7 +13,6 @@
type ctyp
val rep_ctyp: ctyp ->
{thy: theory,
- sign: theory, (*obsolete*)
T: typ,
maxidx: int,
sorts: sort list}
@@ -27,13 +26,11 @@
exception CTERM of string * cterm list
val rep_cterm: cterm ->
{thy: theory,
- sign: theory, (*obsolete*)
t: term,
T: typ,
maxidx: int,
sorts: sort list}
- val crep_cterm: cterm ->
- {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int, sorts: sort list}
+ val crep_cterm: cterm -> {thy: theory, t: term, T: ctyp, maxidx: int, sorts: sort list}
val theory_of_cterm: cterm -> theory
val term_of: cterm -> term
val cterm_of: theory -> term -> cterm
@@ -54,7 +51,6 @@
type attribute (* = Context.generic * thm -> Context.generic * thm *)
val rep_thm: thm ->
{thy: theory,
- sign: theory, (*obsolete*)
der: bool * Proofterm.proof,
tags: tag list,
maxidx: int,
@@ -64,7 +60,6 @@
prop: term}
val crep_thm: thm ->
{thy: theory,
- sign: theory, (*obsolete*)
der: bool * Proofterm.proof,
tags: tag list,
maxidx: int,
@@ -194,7 +189,7 @@
fun rep_ctyp (Ctyp {thy_ref, T, maxidx, sorts}) =
let val thy = Theory.deref thy_ref
- in {thy = thy, sign = thy, T = T, maxidx = maxidx, sorts = sorts} end;
+ in {thy = thy, T = T, maxidx = maxidx, sorts = sorts} end;
fun theory_of_ctyp (Ctyp {thy_ref, ...}) = Theory.deref thy_ref;
@@ -233,11 +228,11 @@
fun rep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
let val thy = Theory.deref thy_ref
- in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
+ in {thy = thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
fun crep_cterm (Cterm {thy_ref, t, T, maxidx, sorts}) =
let val thy = Theory.deref thy_ref in
- {thy = thy, sign = thy, t = t,
+ {thy = thy, t = t,
T = Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts},
maxidx = maxidx, sorts = sorts}
end;
@@ -391,7 +386,7 @@
fun rep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
let val thy = Theory.deref thy_ref in
- {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx,
+ {thy = thy, der = der, tags = tags, maxidx = maxidx,
shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
end;
@@ -401,7 +396,7 @@
val thy = Theory.deref thy_ref;
fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps};
in
- {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
+ {thy = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
hyps = map (cterm ~1) hyps,
tpairs = map (pairself (cterm maxidx)) tpairs,
prop = cterm maxidx prop}
--- a/src/ZF/Tools/cartprod.ML Wed Apr 04 20:22:32 2007 +0200
+++ b/src/ZF/Tools/cartprod.ML Wed Apr 04 23:29:33 2007 +0200
@@ -106,7 +106,7 @@
fun split_rule_var (Var(v,_), Type("fun",[T1,T2]), rl) =
let val T' = factors T1 ---> T2
val newt = ap_split T1 T2 (Var(v,T'))
- val cterm = Thm.cterm_of (#sign(rep_thm rl))
+ val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
in
remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
cterm newt)]) rl)