# HG changeset patch # User wenzelm # Date 1082623952 -7200 # Node ID 130076a81b8414e5101ca0eb61318d8f524b9931 # Parent 2bfe5de2d1fae5c5e87dd81cd3fca9130c7d97fa tuned; diff -r 2bfe5de2d1fa -r 130076a81b84 TFL/rules.ML --- 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)) diff -r 2bfe5de2d1fa -r 130076a81b84 src/FOLP/simp.ML --- 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)) diff -r 2bfe5de2d1fa -r 130076a81b84 src/HOL/Tools/inductive_package.ML --- 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 **) diff -r 2bfe5de2d1fa -r 130076a81b84 src/HOL/Tools/record_package.ML --- 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); diff -r 2bfe5de2d1fa -r 130076a81b84 src/HOLCF/IOA/meta_theory/Sequence.ML --- 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 diff -r 2bfe5de2d1fa -r 130076a81b84 src/HOLCF/adm.ML --- 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)); diff -r 2bfe5de2d1fa -r 130076a81b84 src/HOLCF/domain/library.ML --- 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; diff -r 2bfe5de2d1fa -r 130076a81b84 src/Provers/ind.ML --- 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; diff -r 2bfe5de2d1fa -r 130076a81b84 src/Provers/simp.ML --- 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)) diff -r 2bfe5de2d1fa -r 130076a81b84 src/Pure/Isar/locale.ML --- 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); diff -r 2bfe5de2d1fa -r 130076a81b84 src/Pure/Isar/proof_context.ML --- 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); diff -r 2bfe5de2d1fa -r 130076a81b84 src/Pure/drule.ML --- 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 diff -r 2bfe5de2d1fa -r 130076a81b84 src/Pure/goals.ML --- 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)); diff -r 2bfe5de2d1fa -r 130076a81b84 src/Pure/meta_simplifier.ML --- 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; diff -r 2bfe5de2d1fa -r 130076a81b84 src/Pure/pattern.ML --- 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)); diff -r 2bfe5de2d1fa -r 130076a81b84 src/Pure/unify.ML --- 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;