# HG changeset patch # User wenzelm # Date 1154782377 -7200 # Node ID 4392003fcbfa272f86857b6ed5958d48ad9098d5 # Parent 41e77e688886f2c7babf6916d14f4dc8f3aa10d6 tuned; diff -r 41e77e688886 -r 4392003fcbfa src/ZF/Integ/int_arith.ML --- 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 diff -r 41e77e688886 -r 4392003fcbfa src/ZF/Tools/ind_cases.ML --- 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; diff -r 41e77e688886 -r 4392003fcbfa src/ZF/Tools/inductive_package.ML --- 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)); diff -r 41e77e688886 -r 4392003fcbfa src/ZF/Tools/primrec_package.ML --- 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; diff -r 41e77e688886 -r 4392003fcbfa src/ZF/arith_data.ML --- 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,