--- a/src/ZF/Integ/int_arith.ML Sat Aug 05 14:52:55 2006 +0200
+++ b/src/ZF/Integ/int_arith.ML Sat Aug 05 14:52:57 2006 +0200
@@ -215,7 +215,7 @@
[zmult_assoc, zmult_zminus RS sym, int_minus_mult_eq_1_to_2];
fun prep_simproc (name, pats, proc) =
- Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
+ Simplifier.simproc (the_context ()) name pats proc;
structure CancelNumeralsCommon =
struct
--- a/src/ZF/Tools/ind_cases.ML Sat Aug 05 14:52:55 2006 +0200
+++ b/src/ZF/Tools/ind_cases.ML Sat Aug 05 14:52:57 2006 +0200
@@ -42,7 +42,7 @@
in
(case Symtab.lookup (IndCasesData.get thy) c of
NONE => error ("Unknown inductive cases rule for set " ^ quote c)
- | SOME f => f ss (Thm.cterm_of (Theory.sign_of thy) A))
+ | SOME f => f ss (Thm.cterm_of thy A))
end;
--- a/src/ZF/Tools/inductive_package.ML Sat Aug 05 14:52:55 2006 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Aug 05 14:52:57 2006 +0200
@@ -65,7 +65,6 @@
intr_specs (monos, con_defs, type_intrs, type_elims) thy =
let
val _ = Theory.requires thy "Inductive" "(co)inductive definitions";
- val sign = sign_of thy;
val (intr_names, intr_tms) = split_list (map fst intr_specs);
val case_names = RuleCases.case_names intr_names;
@@ -75,7 +74,7 @@
val dummy = assert_all is_Const rec_hds
(fn t => "Recursive set not previously declared as constant: " ^
- Sign.string_of_term sign t);
+ Sign.string_of_term thy t);
(*Now we know they are all Consts, so get their names, type and params*)
val rec_names = map (#1 o dest_Const) rec_hds
@@ -86,18 +85,18 @@
(fn a => "Base name of recursive set not an identifier: " ^ a);
local (*Checking the introduction rules*)
- val intr_sets = map (#2 o rule_concl_msg sign) intr_tms;
+ val intr_sets = map (#2 o rule_concl_msg thy) intr_tms;
fun intr_ok set =
case head_of set of Const(a,recT) => a mem rec_names | _ => false;
in
val dummy = assert_all intr_ok intr_sets
(fn t => "Conclusion of rule does not name a recursive set: " ^
- Sign.string_of_term sign t);
+ Sign.string_of_term thy t);
end;
val dummy = assert_all is_Free rec_params
(fn t => "Param in recursion term not a free variable: " ^
- Sign.string_of_term sign t);
+ Sign.string_of_term thy t);
(*** Construct the fixedpoint definition ***)
val mk_variant = Name.variant (foldr add_term_names [] intr_tms);
@@ -106,7 +105,7 @@
fun dest_tprop (Const("Trueprop",_) $ P) = P
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
- Sign.string_of_term sign Q);
+ Sign.string_of_term thy Q);
(*Makes a disjunct from an introduction rule*)
fun fp_part intr = (*quantify over rule's free vars except parameters*)
@@ -146,7 +145,7 @@
If no mutual recursion then it equals the one recursive set.
If mutual recursion then it differs from all the recursive sets. *)
val big_rec_base_name = space_implode "_" rec_base_names;
- val big_rec_name = Sign.intern_const sign big_rec_base_name;
+ val big_rec_name = Sign.intern_const thy big_rec_base_name;
val dummy = conditional verbose (fn () =>
@@ -154,7 +153,7 @@
(*Forbid the inductive definition structure from clashing with a theory
name. This restriction may become obsolete as ML is de-emphasized.*)
- val dummy = deny (big_rec_base_name mem (Context.names_of sign))
+ val dummy = deny (big_rec_base_name mem (Context.names_of thy))
("Definition " ^ big_rec_base_name ^
" would clash with the theory of the same name!");
@@ -171,7 +170,7 @@
(*tracing: print the fixedpoint definition*)
val dummy = if !Ind_Syntax.trace then
- List.app (writeln o Sign.string_of_term sign o #2) axpairs
+ List.app (writeln o Sign.string_of_term thy o #2) axpairs
else ()
(*add definitions of the inductive sets*)
@@ -188,13 +187,11 @@
| _ => big_rec_base_name::rec_names);
- val sign1 = sign_of thy1;
-
(********)
val dummy = writeln " Proving monotonicity...";
val bnd_mono =
- Goal.prove_global sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
+ Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
(fn _ => EVERY
[rtac (Collect_subset RS bnd_monoI) 1,
REPEAT (ares_tac (basic_monos @ monos) 1)]);
@@ -252,7 +249,7 @@
val intrs =
(intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
|> ListPair.map (fn (t, tacs) =>
- Goal.prove_global sign1 [] [] t
+ Goal.prove_global thy1 [] [] t
(fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)))
handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg);
@@ -281,7 +278,7 @@
(Thm.assume A RS elim)
|> Drule.standard';
fun mk_cases a = make_cases (*delayed evaluation of body!*)
- (simpset ()) (read_cterm (Thm.sign_of_thm elim) (a, propT));
+ (simpset ()) (read_cterm (Thm.theory_of_thm elim) (a, propT));
fun induction_rules raw_induct thy =
let
@@ -328,7 +325,7 @@
val dummy = if !Ind_Syntax.trace then
(writeln "ind_prems = ";
- List.app (writeln o Sign.string_of_term sign1) ind_prems;
+ List.app (writeln o Sign.string_of_term thy1) ind_prems;
writeln "raw_induct = "; print_thm raw_induct)
else ();
@@ -343,7 +340,7 @@
ORELSE' etac FalseE));
val quant_induct =
- Goal.prove_global sign1 [] ind_prems
+ Goal.prove_global thy1 [] ind_prems
(FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
(fn prems => EVERY
[rewrite_goals_tac part_rec_defs,
@@ -412,9 +409,9 @@
val dummy = if !Ind_Syntax.trace then
(writeln ("induct_concl = " ^
- Sign.string_of_term sign1 induct_concl);
+ Sign.string_of_term thy1 induct_concl);
writeln ("mutual_induct_concl = " ^
- Sign.string_of_term sign1 mutual_induct_concl))
+ Sign.string_of_term thy1 mutual_induct_concl))
else ();
@@ -427,7 +424,7 @@
val lemma = (*makes the link between the two induction rules*)
if need_mutual then
(writeln " Proving the mutual induction rule...";
- Goal.prove_global sign1 [] []
+ Goal.prove_global thy1 [] []
(Logic.mk_implies (induct_concl, mutual_induct_concl))
(fn _ => EVERY
[rewrite_goals_tac part_rec_defs,
@@ -486,7 +483,7 @@
val mutual_induct_fsplit =
if need_mutual then
- Goal.prove_global sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
+ Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
mutual_induct_concl
(fn prems => EVERY
[rtac (quant_induct RS lemma) 1,
@@ -500,8 +497,8 @@
The name "x.1" comes from the "RS spec" !*)
val inst =
case elem_frees of [_] => I
- | _ => instantiate ([], [(cterm_of sign1 (Var(("x",1), Ind_Syntax.iT)),
- cterm_of sign1 elem_tuple)]);
+ | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
+ cterm_of thy1 elem_tuple)]);
(*strip quantifier and the implication*)
val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
--- a/src/ZF/Tools/primrec_package.ML Sat Aug 05 14:52:55 2006 +0200
+++ b/src/ZF/Tools/primrec_package.ML Sat Aug 05 14:52:57 2006 +0200
@@ -91,7 +91,7 @@
#big_rec_name con_info)
else SOME (fname, ftype, ls, rs, con_info, new_eqn::eqns)
end
- handle RecError s => primrec_eq_err (sign_of thy) s eq;
+ handle RecError s => primrec_eq_err thy s eq;
(*Instantiates a recursor equation with constructor arguments*)
@@ -132,11 +132,11 @@
in
if !Ind_Syntax.trace then
writeln ("recursor_rhs = " ^
- Sign.string_of_term (sign_of thy) recursor_rhs ^
- "\nabs = " ^ Sign.string_of_term (sign_of thy) abs)
+ Sign.string_of_term thy recursor_rhs ^
+ "\nabs = " ^ Sign.string_of_term thy abs)
else();
if Logic.occs (fconst, abs) then
- primrec_eq_err (sign_of thy)
+ primrec_eq_err thy
("illegal recursive occurrences of " ^ fname)
eq
else abs :: cases
@@ -159,7 +159,7 @@
in
if !Ind_Syntax.trace then
writeln ("primrec def:\n" ^
- Sign.string_of_term (sign_of thy) def_tm)
+ Sign.string_of_term thy def_tm)
else();
(Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
def_tm)
@@ -197,7 +197,7 @@
fun add_primrec args thy =
add_primrec_i (map (fn ((name, s), srcs) =>
- ((name, Sign.simple_read_term (sign_of thy) propT s), map (Attrib.attribute thy) srcs))
+ ((name, Sign.read_prop thy s), map (Attrib.attribute thy) srcs))
args) thy;
--- a/src/ZF/arith_data.ML Sat Aug 05 14:52:55 2006 +0200
+++ b/src/ZF/arith_data.ML Sat Aug 05 14:52:57 2006 +0200
@@ -79,7 +79,7 @@
end;
fun prep_simproc (name, pats, proc) =
- Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
+ Simplifier.simproc (the_context ()) name pats proc;
(*** Use CancelNumerals simproc without binary numerals,