--- a/TFL/rules.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/TFL/rules.ML Thu Apr 22 10:52:32 2004 +0200
@@ -307,7 +307,7 @@
let val gth = forall_intr v th
val {prop=Const("all",_)$Abs(x,ty,rst),sign,...} = rep_thm gth
val P' = Abs(x,ty, HOLogic.dest_Trueprop rst) (* get rid of trueprop *)
- val tsig = #tsig(Sign.rep_sg sign)
+ val tsig = Sign.tsig_of sign
val theta = Pattern.match tsig (P,P')
val allI2 = instantiate (certify sign theta) allI
val thm = Thm.implies_elim allI2 gth
@@ -712,7 +712,7 @@
val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants1)
val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1
handle U.ERR _ => Thm.reflexive Q1
- val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
+ val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
@@ -778,7 +778,7 @@
fun is_func (Const (name,_)) = (name = func_name)
| is_func _ = false
val rcontext = rev cntxt
- val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
+ val cncl = HOLogic.dest_Trueprop o Thm.prop_of
val antl = case rcontext of [] => []
| _ => [S.list_mk_conj(map cncl rcontext)]
val TC = genl(S.list_mk_imp(antl, A))
--- a/src/FOLP/simp.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/FOLP/simp.ML Thu Apr 22 10:52:32 2004 +0200
@@ -556,7 +556,7 @@
in find subst_thms end;
fun mk_cong sg (f,aTs,rT) (refl,eq) =
-let val tsig = #tsig(Sign.rep_sg sg);
+let val tsig = Sign.tsig_of sg;
val k = length aTs;
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
let val ca = cterm_of sg va
@@ -578,7 +578,7 @@
fun mk_cong_type sg (f,T) =
let val (aTs,rT) = strip_type T;
- val tsig = #tsig(Sign.rep_sg sg);
+ val tsig = Sign.tsig_of sg;
fun find_refl(r::rs) =
let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
--- a/src/HOL/Tools/inductive_package.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/HOL/Tools/inductive_package.ML Thu Apr 22 10:52:32 2004 +0200
@@ -178,7 +178,7 @@
same type in all introduction rules*)
fun unify_consts sign cs intr_ts =
(let
- val {tsig, ...} = Sign.rep_sg sign;
+ val tsig = Sign.tsig_of sign;
val add_term_consts_2 =
foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
fun varify (t, (i, ts)) =
@@ -264,7 +264,7 @@
fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
let val T' = prodT_factors [] ps T1 ---> T2
val newt = ap_split [] ps T1 T2 (Var (v, T'))
- val cterm = Thm.cterm_of (#sign (rep_thm rl))
+ val cterm = Thm.cterm_of (Thm.sign_of_thm rl)
in
instantiate ([], [(cterm t, cterm newt)]) rl
end
@@ -273,11 +273,11 @@
val remove_split = rewrite_rule [split_conv RS eq_reflection];
fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
- (mg_prod_factors vs ([], #prop (rep_thm rl)), rl)));
+ (mg_prod_factors vs ([], Thm.prop_of rl), rl)));
fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
(mapfilter (fn (t as Var ((a, _), _)) =>
- apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl)));
+ apsome (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)), rl)));
(** process rules **)
--- a/src/HOL/Tools/record_package.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/HOL/Tools/record_package.ML Thu Apr 22 10:52:32 2004 +0200
@@ -107,7 +107,7 @@
fun try_param_tac s rule i st =
let
- val cert = cterm_of (#sign (rep_thm st));
+ val cert = cterm_of (Thm.sign_of_thm st);
val g = nth_elem (i - 1, prems_of st);
val params = Logic.strip_params g;
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
@@ -364,8 +364,8 @@
Some s => s
| None => Sign.defaultS sg);
- val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm)
- val {tsig,...} = Sign.rep_sg sg
+ val T = Sign.intern_typ sg (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts tm)) I tm);
+ val tsig = Sign.tsig_of sg;
fun mk_type_abbr subst name alphas =
let val abbrT = Type (name, map (fn a => TVar ((a,0),logicS)) alphas);
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Thu Apr 22 10:52:32 2004 +0200
@@ -1012,7 +1012,7 @@
(*Generalizes over all free variables, with the named var outermost.*)
fun all_frees_tac x i thm =
let
- val tsig = #tsig (Sign.rep_sg (#sign (rep_thm thm)));
+ val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
val frees = add_frees tsig (nth_elem (i - 1, prems_of thm), [x]);
val frees' = sort (op >) (frees \ x) @ [x];
in
--- a/src/HOLCF/adm.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/HOLCF/adm.ML Thu Apr 22 10:52:32 2004 +0200
@@ -114,7 +114,7 @@
fun inst_adm_subst_thm state i params s T subt t paths =
let val {sign, maxidx, ...} = rep_thm state;
val j = maxidx+1;
- val {tsig, ...} = Sign.rep_sg sign;
+ val tsig = Sign.tsig_of sign;
val parTs = map snd (rev params);
val rule = lift_rule (state, i) adm_subst;
val types = the o (fst (types_sorts rule));
--- a/src/HOLCF/domain/library.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/HOLCF/domain/library.ML Thu Apr 22 10:52:32 2004 +0200
@@ -75,7 +75,6 @@
fun rep_Type (Type x) = x | rep_Type _ = Imposs "library:rep_Type";
fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree";
-val tsig_of = #tsig o Sign.rep_sg;
fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
--- a/src/Provers/ind.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Provers/ind.ML Thu Apr 22 10:52:32 2004 +0200
@@ -41,7 +41,7 @@
(*Generalizes over all free variables, with the named var outermost.*)
fun all_frees_tac (var:string) i thm =
- let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
+ let val tsig = Sign.tsig_of (Thm.sign_of_thm thm);
val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
in foldl (qnt_tac i) (all_tac,frees') thm end;
--- a/src/Provers/simp.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Provers/simp.ML Thu Apr 22 10:52:32 2004 +0200
@@ -582,7 +582,7 @@
in find subst_thms end;
fun mk_cong sg (f,aTs,rT) (refl,eq) =
-let val tsig = #tsig(Sign.rep_sg sg);
+let val tsig = Sign.tsig_of sg;
val k = length aTs;
fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
let val ca = cterm_of sg va
@@ -604,7 +604,7 @@
fun mk_cong_type sg (f,T) =
let val (aTs,rT) = strip_type T;
- val tsig = #tsig(Sign.rep_sg sg);
+ val tsig = Sign.tsig_of sg;
fun find_refl(r::rs) =
let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
in if Type.typ_instance(tsig, rT, hd(binder_types eqT))
--- a/src/Pure/Isar/locale.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Pure/Isar/locale.ML Thu Apr 22 10:52:32 2004 +0200
@@ -635,7 +635,8 @@
|> Drule.implies_intr_list (Library.drop (length axs, hyps))
|> Seq.single;
-fun activate_elem _ ((ctxt, axs), Fixes fixes) = ((ctxt |> ProofContext.add_fixes fixes, axs), [])
+fun activate_elem _ ((ctxt, axs), Fixes fixes) =
+ ((ctxt |> ProofContext.add_fixes fixes, axs), [])
| activate_elem _ ((ctxt, axs), Assumes asms) =
let
val ts = flat (map (map #1 o #2) asms);
--- a/src/Pure/Isar/proof_context.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Apr 22 10:52:32 2004 +0200
@@ -19,7 +19,6 @@
val prems_of: context -> thm list
val print_proof_data: theory -> unit
val init: theory -> context
- val add_syntax: (string * typ option * mixfix option) list -> context -> context
val is_fixed: context -> string -> bool
val default_type: context -> string -> typ option
val used_types: context -> string list
@@ -105,7 +104,7 @@
val fix: (string list * string option) list -> context -> context
val fix_i: (string list * typ option) list -> context -> context
val fix_direct: (string list * typ option) list -> context -> context
- val add_fixes: (string * typ option * mixfix option) list -> context -> context
+ val add_fixes: (string * typ option * Syntax.mixfix option) list -> context -> context
val fix_frees: term list -> context -> context
val bind_skolem: context -> string list -> term -> term
val get_case: context -> string -> string option list -> RuleCases.T
@@ -1223,8 +1222,6 @@
end;
-(* CB: fix free variables occuring in ts, unless already fixed. *)
-
fun fix_frees ts ctxt =
let
val frees = foldl Term.add_frees ([], ts);
--- a/src/Pure/drule.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Pure/drule.ML Thu Apr 22 10:52:32 2004 +0200
@@ -748,7 +748,7 @@
(*Instantiate theorem th, reading instantiations under theory of th*)
fun read_instantiate sinsts th =
- read_instantiate_sg (#sign (rep_thm th)) sinsts th;
+ read_instantiate_sg (Thm.sign_of_thm th) sinsts th;
(*Left-to-right replacements: tpairs = [...,(vi,ti),...].
@@ -759,12 +759,12 @@
and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
val maxi = Int.max(maxidx, Int.max(maxt, maxu));
val sign' = Sign.merge(sign, Sign.merge(signt, signu))
- val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) (tye, maxi) (T, U)
+ val (tye',maxi') = Type.unify (Sign.tsig_of sign') (tye, maxi) (T, U)
handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
in (sign', tye', maxi') end;
in
fun cterm_instantiate ctpairs0 th =
- let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th), Vartab.empty, 0))
+ let val (sign,tye,_) = foldr add_types (ctpairs0, (Thm.sign_of_thm th, Vartab.empty, 0))
fun instT(ct,cu) =
let val inst = cterm_of sign o subst_TVars_Vartab tye o term_of
in (inst ct, inst cu) end
--- a/src/Pure/goals.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Pure/goals.ML Thu Apr 22 10:52:32 2004 +0200
@@ -707,7 +707,7 @@
fun get_top_scope_thms thy =
let val sc = (get_scope_sg (Theory.sign_of thy))
in if (null sc) then (warning "No locale in theory"; [])
- else map (#prop o rep_thm) (map #2 (#thms(snd(hd sc))))
+ else map Thm.prop_of (map #2 (#thms(snd(hd sc))))
end;
fun implies_intr_some_hyps thy A_set th =
@@ -778,16 +778,16 @@
(map (Sign.string_of_term sign)
(filter (fn x => (not (in_locale [x] sign)))
hyps)))
- else if Pattern.matches (#tsig(Sign.rep_sg sign))
+ else if Pattern.matches (Sign.tsig_of sign)
(Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
then final_th
else !result_error_fn state "proved a different theorem"
end
in
- if Sign.eq_sg(sign, #sign(rep_thm st0))
+ if Sign.eq_sg(sign, Thm.sign_of_thm st0)
then (prems, st0, mkresult)
else error ("Definitions would change the proof state's signature" ^
- sign_error (sign, #sign(rep_thm st0)))
+ sign_error (sign, Thm.sign_of_thm st0))
end
handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s);
@@ -994,7 +994,7 @@
then warning "Warning: same as previous level"
else if eq_thm_sg(th,th2) then ()
else warning ("Warning: signature of proof state has changed" ^
- sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
+ sign_error (Thm.sign_of_thm th, Thm.sign_of_thm th2));
((th2,ths2)::(th,ths)::pairs)));
fun by tac = cond_timeit (!Library.timing)
@@ -1096,7 +1096,7 @@
(** Reading and printing terms wrt the current theory **)
-fun top_sg() = #sign(rep_thm(topthm()));
+fun top_sg() = Thm.sign_of_thm (topthm());
fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
--- a/src/Pure/meta_simplifier.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Pure/meta_simplifier.ML Thu Apr 22 10:52:32 2004 +0200
@@ -283,7 +283,7 @@
(exists (apl (lhs, Logic.occs)) (rhs :: prems))
orelse
(null prems andalso
- Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs))
+ Pattern.matches (Sign.tsig_of sign) (lhs, rhs))
(*the condition "null prems" is necessary because conditional rewrites
with extra variables in the conditions may terminate although
the rhs is an instance of the lhs. Example: ?m < ?n ==> f(?n) == f(?m)*)
@@ -630,7 +630,7 @@
val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
else Thm.cterm_match (elhs', eta_t');
val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
- val prop' = #prop (rep_thm thm');
+ val prop' = Thm.prop_of thm';
val unconditional = (Logic.count_prems (prop',0) = 0);
val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
in
@@ -666,7 +666,7 @@
in case opt of None => rews rrules | some => some end;
fun sort_rrules rrs = let
- fun is_simple({thm, ...}:rrule) = case #prop (rep_thm thm) of
+ fun is_simple({thm, ...}:rrule) = case Thm.prop_of thm of
Const("==",_) $ _ $ _ => true
| _ => false
fun sort [] (re1,re2) = re1 @ re2
@@ -701,7 +701,7 @@
(* conversion to apply a congruence rule to a term *)
fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
- let val {sign, ...} = rep_thm cong
+ let val sign = Thm.sign_of_thm cong
val _ = if Sign.subsig (sign, signt) then ()
else error("Congruence rule from different theory")
val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
--- a/src/Pure/pattern.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Pure/pattern.ML Thu Apr 22 10:52:32 2004 +0200
@@ -287,7 +287,7 @@
in Envir.update((F,mkabs(binders,is,u)),env') end
handle Unif => (proj_fail params; raise Unif));
-fun unify(sg,env,tus) = (sgr := sg; tsgr := #tsig(Sign.rep_sg sg);
+fun unify(sg,env,tus) = (sgr := sg; tsgr := Sign.tsig_of sg;
foldl (unif []) (env,tus));
--- a/src/Pure/unify.ML Thu Apr 22 10:49:30 2004 +0200
+++ b/src/Pure/unify.ML Thu Apr 22 10:52:32 2004 +0200
@@ -179,7 +179,7 @@
fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
if T=U then env
- else let val (iTs',maxidx') = Type.unify (#tsig(Sign.rep_sg (!sgr))) (iTs, maxidx) (U, T)
+ else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (!sgr)) (iTs, maxidx) (U, T)
in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
handle Type.TUNIFY => raise CANTUNIFY;