# HG changeset patch # User wenzelm # Date 1175722173 -7200 # Node ID d0d2af4db18f497729b8327e0720508079704498 # Parent 293934e41dfd48b607da56d1c4342f9e2aa4ff69 rep_thm/cterm/ctyp: removed obsolete sign field; diff -r 293934e41dfd -r d0d2af4db18f TFL/dcterm.ML --- 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; diff -r 293934e41dfd -r d0d2af4db18f TFL/post.ML --- 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 *) diff -r 293934e41dfd -r d0d2af4db18f TFL/rules.ML --- 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) diff -r 293934e41dfd -r d0d2af4db18f src/FOLP/simp.ML --- 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 diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Import/proof_kernel.ML --- 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 diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Modelcheck/MuckeSyn.ML --- 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; diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Modelcheck/mucke_oracle.ML --- 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; diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Tools/datatype_aux.ML --- 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 diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Tools/datatype_realizer.ML --- 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; diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Tools/datatype_rep_proofs.ML --- 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, diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Tools/inductive_realizer.ML --- 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) diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Tools/record_package.ML --- 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 diff -r 293934e41dfd -r d0d2af4db18f src/HOL/Tools/res_axioms.ML --- 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 diff -r 293934e41dfd -r d0d2af4db18f src/HOLCF/IOA/Modelcheck/MuIOAOracle.ML --- 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; diff -r 293934e41dfd -r d0d2af4db18f src/HOLCF/adm_tac.ML --- 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; diff -r 293934e41dfd -r d0d2af4db18f src/Provers/Arith/fast_lin_arith.ML --- 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 diff -r 293934e41dfd -r d0d2af4db18f src/Provers/blast.ML --- 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 diff -r 293934e41dfd -r d0d2af4db18f src/Provers/splitter.ML --- 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)); diff -r 293934e41dfd -r d0d2af4db18f src/Pure/Proof/extraction.ML --- 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); diff -r 293934e41dfd -r d0d2af4db18f src/Pure/codegen.ML --- 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)); diff -r 293934e41dfd -r d0d2af4db18f src/Pure/tctical.ML --- 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; diff -r 293934e41dfd -r d0d2af4db18f src/Pure/thm.ML --- 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} diff -r 293934e41dfd -r d0d2af4db18f src/ZF/Tools/cartprod.ML --- 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)