--- a/src/HOL/Import/import_syntax.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Import/import_syntax.ML Tue Sep 25 17:06:14 2007 +0200
@@ -45,7 +45,7 @@
val import_theory = P.name >> (fn thyname =>
fn thy =>
thy |> set_generating_thy thyname
- |> Theory.add_path thyname
+ |> Sign.add_path thyname
|> add_dump (";setup_theory " ^ thyname))
fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
@@ -80,7 +80,7 @@
|> replay
|> clear_used_names
|> export_hol4_pending
- |> Theory.parent_path
+ |> Sign.parent_path
|> dump_import_thy thyname
|> add_dump ";end_setup"
end) toks
@@ -175,7 +175,7 @@
fun apply [] thy = thy
| apply (f::fs) thy = apply fs (f thy)
in
- apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
+ apply (set_replaying_thy s::Sign.add_path s::(fst (importP token_list)))
end
fun create_int_thms thyname thy =
@@ -215,7 +215,7 @@
thy |> set_segment thyname segname
|> clear_import_thy
|> clear_int_thms
- |> Theory.parent_path
+ |> Sign.parent_path
end) toks
val set_dump = P.string -- P.string >> setup_dump
--- a/src/HOL/Import/proof_kernel.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Import/proof_kernel.ML Tue Sep 25 17:06:14 2007 +0200
@@ -1928,7 +1928,7 @@
val csyn = mk_syn thy constname
val thy1 = case HOL4DefThy.get thy of
Replaying _ => thy
- | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Theory.add_consts_i [(constname,ctype,csyn)] thy)
+ | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
val eq = mk_defeq constname rhs' thy1
val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
val _ = ImportRecorder.add_defs thmname eq
@@ -2019,7 +2019,7 @@
val thy' = add_dump str thy
val _ = ImportRecorder.add_consts consts
in
- Theory.add_consts_i consts thy'
+ Sign.add_consts_i consts thy'
end
val thy1 = foldr (fn(name,thy)=>
--- a/src/HOL/Import/replay.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Import/replay.ML Tue Sep 25 17:06:14 2007 +0200
@@ -334,7 +334,7 @@
add_hol4_mapping thyname thmname isaname thy
| delta (Hol_pending (thyname, thmname, th)) thy =
add_hol4_pending thyname thmname ([], th_of thy th) thy
- | delta (Consts cs) thy = Theory.add_consts_i cs thy
+ | delta (Consts cs) thy = Sign.add_consts_i cs thy
| delta (Hol_const_mapping (thyname, constname, fullcname)) thy =
add_hol4_const_mapping thyname constname true fullcname thy
| delta (Hol_move (fullname, moved_thmname)) thy =
--- a/src/HOL/Nominal/nominal_atoms.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Tue Sep 25 17:06:14 2007 +0200
@@ -163,7 +163,7 @@
cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
in
- thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)]
+ thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)]
|> PureThy.add_defs_unchecked_i true [((name, def2),[])]
|> snd
|> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
@@ -193,7 +193,7 @@
(Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
in
- thy |> Theory.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)]
+ thy |> Sign.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)]
|> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
end) ak_names_types thy3;
--- a/src/HOL/Nominal/nominal_inductive.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Tue Sep 25 17:06:14 2007 +0200
@@ -419,7 +419,7 @@
else (strong_raw_induct RSN (2, rev_mp),
[ind_case_names, RuleCases.consumes 1]);
val ([strong_induct'], thy') = thy |>
- Theory.add_path rec_name |>
+ Sign.add_path rec_name |>
PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)];
val strong_inducts =
ProjectRule.projects ctxt (1 upto length names) strong_induct'
@@ -427,7 +427,7 @@
thy' |>
PureThy.add_thmss [(("strong_inducts", strong_inducts),
[ind_case_names, RuleCases.consumes 1])] |> snd |>
- Theory.parent_path
+ Sign.parent_path
end))
(map (map (rulify_term thy #> rpair [])) vc_compat)
end;
@@ -506,9 +506,9 @@
end) atoms
in
fold (fn (name, ths) =>
- Theory.add_path (Sign.base_name name) #>
+ Sign.add_path (Sign.base_name name) #>
PureThy.add_thmss [(("eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #>
- Theory.parent_path) (names ~~ transp thss) thy
+ Sign.parent_path) (names ~~ transp thss) thy
end;
--- a/src/HOL/Nominal/nominal_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -235,7 +235,7 @@
val tmp_thy = thy |>
Theory.copy |>
- Theory.add_types (map (fn (tvs, tname, mx, _) =>
+ Sign.add_types (map (fn (tvs, tname, mx, _) =>
(tname, length tvs, mx)) dts);
val atoms = atoms_of thy;
@@ -330,7 +330,7 @@
end) descr);
val (perm_simps, thy2) = thy1 |>
- Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
+ Sign.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
(List.drop (perm_names_types, length new_type_names))) |>
PrimrecPackage.add_primrec_unchecked_i "" perm_eqs;
@@ -820,7 +820,7 @@
(Const (rep_name, T --> T') $ lhs, rhs));
val def_name = (Sign.base_name cname) ^ "_def";
val ([def_thm], thy') = thy |>
- Theory.add_consts_i [(cname', constrT, mx)] |>
+ Sign.add_consts_i [(cname', constrT, mx)] |>
(PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
in (thy', defs @ [def_thm], eqns @ [eqn]) end;
@@ -831,7 +831,7 @@
(Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
- ((Theory.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
+ ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
in
(parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
end;
@@ -1128,10 +1128,10 @@
val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, NominalThmDecls.eqvt_add];
val (_, thy9) = thy8 |>
- Theory.add_path big_name |>
+ Sign.add_path big_name |>
PureThy.add_thms [(("weak_induct", dt_induct), [case_names_induct])] ||>>
PureThy.add_thmss [(("weak_inducts", projections dt_induct), [case_names_induct])] ||>
- Theory.parent_path ||>>
+ Sign.parent_path ||>>
DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
DatatypeAux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
@@ -1409,7 +1409,7 @@
(etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
val (_, thy10) = thy9 |>
- Theory.add_path big_name |>
+ Sign.add_path big_name |>
PureThy.add_thms [(("induct'", induct_aux), [])] ||>>
PureThy.add_thms [(("induct", induct), [case_names_induct])] ||>>
PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])];
@@ -2022,7 +2022,7 @@
val (reccomb_defs, thy12) =
thy11
- |> Theory.add_consts_i (map (fn ((name, T), T') =>
+ |> Sign.add_consts_i (map (fn ((name, T), T') =>
(Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
@@ -2067,7 +2067,7 @@
(("rec_fresh", List.concat rec_fresh_thms), []),
(("rec_unique", map standard rec_unique_thms), []),
(("recs", rec_thms), [])] ||>
- Theory.parent_path ||>
+ Sign.parent_path ||>
map_nominal_datatypes (fold Symtab.update dt_infos);
in
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Sep 25 17:06:14 2007 +0200
@@ -275,7 +275,7 @@
if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
val (defs_thms', thy') =
thy
- |> Theory.add_path primrec_name
+ |> Sign.add_path primrec_name
|> fold_map def (map (fn ((name, t), _) => ((name, []), t)) defs');
val cert = cterm_of thy';
@@ -369,7 +369,7 @@
thy'
|> note (("simps", [Simplifier.simp_add]), simps'')
|> snd
- |> Theory.parent_path
+ |> Sign.parent_path
end))
[goals] |>
Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Sep 25 17:06:14 2007 +0200
@@ -234,7 +234,7 @@
val (reccomb_defs, thy2) =
thy1
- |> Theory.add_consts_i (map (fn ((name, T), T') =>
+ |> Sign.add_consts_i (map (fn ((name, T), T') =>
(Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts))
|> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
@@ -260,9 +260,9 @@
in
thy2
- |> Theory.add_path (space_implode "_" new_type_names)
+ |> Sign.add_path (space_implode "_" new_type_names)
|> PureThy.add_thmss [(("recs", rec_thms), [])]
- ||> Theory.parent_path
+ ||> Sign.parent_path
|-> (fn thms => pair (reccomb_names, Library.flat thms))
end;
--- a/src/HOL/Tools/datatype_aux.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Tue Sep 25 17:06:14 2007 +0200
@@ -70,26 +70,26 @@
val quiet_mode = ref false;
fun message s = if !quiet_mode then () else writeln s;
-fun add_path flat_names s = if flat_names then I else Theory.add_path s;
-fun parent_path flat_names = if flat_names then I else Theory.parent_path;
+fun add_path flat_names s = if flat_names then I else Sign.add_path s;
+fun parent_path flat_names = if flat_names then I else Sign.parent_path;
(* store theorems in theory *)
fun store_thmss_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Theory.add_path tname
+ Sign.add_path tname
#> PureThy.add_thmss [((label, thms), atts)]
- #-> (fn thm::_ => Theory.parent_path #> pair thm)
+ #-> (fn thm::_ => Sign.parent_path #> pair thm)
) (tnames ~~ attss ~~ thmss);
fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
fun store_thms_atts label tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Theory.add_path tname
+ Sign.add_path tname
#> PureThy.add_thms [((label, thms), atts)]
- #-> (fn thm::_ => Theory.parent_path #> pair thm)
+ #-> (fn thm::_ => Sign.parent_path #> pair thm)
) (tnames ~~ attss ~~ thmss);
fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
--- a/src/HOL/Tools/datatype_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -422,14 +422,14 @@
(datatype_of_case (ProofContext.theory_of ctxt));
fun add_case_tr' case_names thy =
- Theory.add_advanced_trfuns ([], [],
+ Sign.add_advanced_trfuns ([], [],
map (fn case_name =>
let val case_name' = Sign.const_syntax_name thy case_name
in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
end) case_names, []) thy;
val trfun_setup =
- Theory.add_advanced_trfuns ([],
+ Sign.add_advanced_trfuns ([],
[("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
[], []);
@@ -490,9 +490,9 @@
fun add_and_get_axioms_atts label tnames ts attss =
fold_map (fn (tname, (atts, t)) => fn thy =>
thy
- |> Theory.add_path tname
+ |> Sign.add_path tname
|> add_axiom label t atts
- ||> Theory.parent_path
+ ||> Sign.parent_path
|-> (fn [ax] => pair ax)) (tnames ~~ (attss ~~ ts));
fun add_and_get_axioms label tnames ts =
@@ -501,9 +501,9 @@
fun add_and_get_axiomss label tnames tss =
fold_map (fn (tname, ts) => fn thy =>
thy
- |> Theory.add_path tname
+ |> Sign.add_path tname
|> add_axioms label ts []
- ||> Theory.parent_path
+ ||> Sign.parent_path
|-> (fn [ax] => pair ax)) (tnames ~~ tss);
fun gen_specify_consts add args thy =
@@ -594,10 +594,10 @@
val ((([induct], [rec_thms]), inject), thy3) =
thy2
- |> Theory.add_path (space_implode "_" new_type_names)
+ |> Sign.add_path (space_implode "_" new_type_names)
|> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct]
||>> add_axioms "recs" rec_axs []
- ||> Theory.parent_path
+ ||> Sign.parent_path
||>> add_and_get_axiomss "inject" new_type_names
(DatatypeProp.make_injs descr sorts);
val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names
@@ -632,12 +632,12 @@
val thy12 =
thy11
|> add_case_tr' case_names'
- |> Theory.add_path (space_implode "_" new_type_names)
+ |> Sign.add_path (space_implode "_" new_type_names)
|> add_rules simps case_thms rec_thms inject distinct
weak_case_congs Simplifier.cong_add
|> put_dt_infos dt_infos
|> add_cases_induct dt_infos induct
- |> Theory.parent_path
+ |> Sign.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
|> snd
|> DatatypeInterpretation.data (map fst dt_infos);
@@ -690,12 +690,12 @@
val thy12 =
thy10
|> add_case_tr' case_names
- |> Theory.add_path (space_implode "_" new_type_names)
+ |> Sign.add_path (space_implode "_" new_type_names)
|> add_rules simps case_thms rec_thms inject distinct
weak_case_congs (Simplifier.attrib (op addcongs))
|> put_dt_infos dt_infos
|> add_cases_induct dt_infos induct
- |> Theory.parent_path
+ |> Sign.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
|> DatatypeInterpretation.data (map fst dt_infos);
in
@@ -778,7 +778,7 @@
thy8
|> store_thmss "inject" new_type_names inject
||>> store_thmss "distinct" new_type_names distinct
- ||> Theory.add_path (space_implode "_" new_type_names)
+ ||> Sign.add_path (space_implode "_" new_type_names)
||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
val dt_infos = map (make_dt_info (length descr) descr sorts induction'
@@ -795,7 +795,7 @@
weak_case_congs (Simplifier.attrib (op addcongs))
|> put_dt_infos dt_infos
|> add_cases_induct dt_infos induction'
- |> Theory.parent_path
+ |> Sign.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
|> snd
|> DatatypeInterpretation.data (map fst dt_infos);
@@ -825,7 +825,7 @@
val tmp_thy = thy |>
Theory.copy |>
- Theory.add_types (map (fn (tvs, tname, mx, _) =>
+ Sign.add_types (map (fn (tvs, tname, mx, _) =>
(tname, length tvs, mx)) dts);
val (tyvars, _, _, _)::_ = dts;
--- a/src/HOL/Tools/datatype_realizer.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Tue Sep 25 17:06:14 2007 +0200
@@ -130,10 +130,10 @@
val ind_name = Thm.get_name induction;
val vs = map (fn i => List.nth (pnames, i)) is;
val (thm', thy') = thy
- |> Theory.absolute_path
+ |> Sign.absolute_path
|> PureThy.store_thm
((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
- ||> Theory.restore_naming thy;
+ ||> Sign.restore_naming thy;
val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
@@ -197,9 +197,9 @@
val exh_name = Thm.get_name exhaustion;
val (thm', thy') = thy
- |> Theory.absolute_path
+ |> Sign.absolute_path
|> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
- ||> Theory.restore_naming thy;
+ ||> Sign.restore_naming thy;
val P = Var (("P", 0), rT' --> HOLogic.boolT);
val prf = forall_intr_prf (y, forall_intr_prf (P,
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 25 17:06:14 2007 +0200
@@ -236,7 +236,7 @@
(Const (rep_name, T --> Univ_elT) $ lhs, rhs));
val ([def_thm], thy') =
thy
- |> Theory.add_consts_i [(cname', constrT, mx)]
+ |> Sign.add_consts_i [(cname', constrT, mx)]
|> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
@@ -259,7 +259,7 @@
end;
val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
- ((thy3 |> Theory.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
+ ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
(*********** isomorphisms for new types (introduced by typedef) ***********)
@@ -616,9 +616,9 @@
val ([dt_induct'], thy7) =
thy6
- |> Theory.add_path big_name
+ |> Sign.add_path big_name
|> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
- ||> Theory.parent_path;
+ ||> Sign.parent_path;
in
((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
--- a/src/HOL/Tools/inductive_realizer.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Tue Sep 25 17:06:14 2007 +0200
@@ -292,14 +292,14 @@
val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
val thy1 = thy |>
- Theory.root_path |>
- Theory.add_path (NameSpace.implode prfx);
+ Sign.root_path |>
+ Sign.add_path (NameSpace.implode prfx);
val (ty_eqs, rlz_eqs) = split_list
(map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
val thy1' = thy1 |>
Theory.copy |>
- Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
+ Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
fold (fn s => AxClass.axiomatize_arity_i
(s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
Extraction.add_typeof_eqns_i ty_eqs;
@@ -355,7 +355,7 @@
((Sign.base_name (name_of_thm intr), []),
subst_atomic rlzpreds' (Logic.unvarify rintr)))
(rintrs ~~ maps snd rss)) [] ||>
- Theory.absolute_path;
+ Sign.absolute_path;
val thy3 = PureThy.hide_thms false
(map name_of_thm (#intrs ind_info)) thy3';
@@ -480,7 +480,7 @@
(HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
- in Theory.restore_naming thy thy6 end;
+ in Sign.restore_naming thy thy6 end;
fun add_ind_realizers name rsets thy =
let
--- a/src/HOL/Tools/numeral_syntax.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Tue Sep 25 17:06:14 2007 +0200
@@ -88,7 +88,7 @@
(* theory setup *)
val setup =
- Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
- Theory.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
+ Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
+ Sign.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
end;
--- a/src/HOL/Tools/primrec_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -285,7 +285,7 @@
if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
val (defs_thms', thy') =
thy
- |> Theory.add_path primrec_name
+ |> Sign.add_path primrec_name
|> fold_map def (map (fn (name, t) => ((name, []), t)) defs');
val rewrites = (map mk_meta_eq rec_rewrites) @ map snd defs_thms';
val _ = message ("Proving equations for primrec function(s) " ^
@@ -302,7 +302,7 @@
|> snd
|> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
|> snd
- |> Theory.parent_path
+ |> Sign.parent_path
|> pair simps''
end;
--- a/src/HOL/Tools/recdef_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/recdef_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -215,7 +215,7 @@
val ((simps' :: rules', [induct']), thy) =
thy
- |> Theory.add_path bname
+ |> Sign.add_path bname
|> PureThy.add_thmss
((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
||>> PureThy.add_thms [(("induct", induct), [])];
@@ -223,7 +223,7 @@
val thy =
thy
|> put_recdef name result
- |> Theory.parent_path;
+ |> Sign.parent_path;
in (thy, result) end;
val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
@@ -245,9 +245,9 @@
val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
val ([induct_rules'], thy3) =
thy2
- |> Theory.add_path bname
+ |> Sign.add_path bname
|> PureThy.add_thms [(("induct_rules", induct_rules), [])]
- ||> Theory.parent_path;
+ ||> Sign.parent_path;
in (thy3, {induct_rules = induct_rules'}) end;
val defer_recdef = gen_defer_recdef Tfl.defer IsarCmd.apply_theorems;
--- a/src/HOL/Tools/record_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -1507,7 +1507,7 @@
fun mk_defs () =
thy
|> extension_typedef name repT (alphas@[zeta])
- ||> Theory.add_consts_i
+ ||> Sign.add_consts_i
(map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
@@ -1780,7 +1780,7 @@
(* 1st stage: extension_thy *)
val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split,u_convs) =
thy
- |> Theory.add_path bname
+ |> Sign.add_path bname
|> extension_definition full extN fields names alphas_ext zeta moreT more vars;
val _ = timing_msg "record preparing definitions";
@@ -1900,16 +1900,16 @@
fun mk_defs () =
extension_thy
- |> Theory.add_trfuns
+ |> Sign.add_trfuns
([],[],field_tr's, [])
- |> Theory.add_advanced_trfuns
+ |> Sign.add_advanced_trfuns
([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
- |> Theory.parent_path
- |> Theory.add_tyabbrs_i recordT_specs
- |> Theory.add_path bname
- |> Theory.add_consts_i
+ |> Sign.parent_path
+ |> Sign.add_tyabbrs_i recordT_specs
+ |> Sign.add_path bname
+ |> Sign.add_consts_i
(map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
- |> (Theory.add_consts_i o map Syntax.no_syn)
+ |> (Sign.add_consts_i o map Syntax.no_syn)
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
|> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
@@ -2169,7 +2169,7 @@
|> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
|> add_extfields extension_name (fields @ [(full_moreN,moreT)])
|> add_fieldext (extension_name,snd extension) (names @ [full_moreN])
- |> Theory.parent_path;
+ |> Sign.parent_path;
in final_thy
end;
@@ -2263,8 +2263,8 @@
(* setup theory *)
val setup =
- Theory.add_trfuns ([], parse_translation, [], []) #>
- Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
+ Sign.add_trfuns ([], parse_translation, [], []) #>
+ Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
(fn thy => (Simplifier.change_simpset_of thy
(fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy));
--- a/src/HOL/Tools/string_syntax.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/string_syntax.ML Tue Sep 25 17:06:14 2007 +0200
@@ -77,7 +77,7 @@
(* theory setup *)
val setup =
- Theory.add_trfuns
+ Sign.add_trfuns
([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [],
[("Char", char_ast_tr'), ("@list", list_ast_tr')]);
--- a/src/HOL/Tools/typedef_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -54,8 +54,8 @@
fun add_typedecls decls thy =
if can (Theory.assert_super HOL.thy) thy then
- thy |> Theory.add_typedecls decls |> fold HOL_arity decls
- else thy |> Theory.add_typedecls decls;
+ thy |> Sign.add_typedecls decls |> fold HOL_arity decls
+ else thy |> Sign.add_typedecls decls;
@@ -151,7 +151,7 @@
fun typedef_result nonempty =
add_typedecls [(t, vs, mx)]
- #> Theory.add_consts_i
+ #> Sign.add_consts_i
((if def then [(name, setT', NoSyn)] else []) @
[(Rep_name, newT --> oldT, NoSyn),
(Abs_name, oldT --> newT, NoSyn)])
@@ -168,7 +168,7 @@
val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
thy1
- |> Theory.add_path name
+ |> Sign.add_path name
|> PureThy.add_thms
([((Rep_name, make Rep), []),
((Rep_name ^ "_inverse", make Rep_inverse), []),
@@ -183,7 +183,7 @@
[RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]),
((Abs_name ^ "_induct", make Abs_induct),
[RuleCases.case_names [Abs_name], InductAttrib.induct_type full_tname])])
- ||> Theory.parent_path;
+ ||> Sign.parent_path;
val info = {rep_type = oldT, abs_type = newT,
Rep_name = full Rep_name, Abs_name = full Abs_name,
type_definition = type_definition, set_def = set_def,
--- a/src/HOLCF/Tools/domain/domain_axioms.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML Tue Sep 25 17:06:14 2007 +0200
@@ -156,14 +156,14 @@
::map one_con cons))));
in foldr1 mk_conj (mapn one_comp 0 eqs)end ));
fun add_one (thy,(dnam,axs,dfs)) = thy
- |> Theory.add_path dnam
+ |> Sign.add_path dnam
|> add_defs_infer dfs
|> add_axioms_infer axs
- |> Theory.parent_path;
+ |> Sign.parent_path;
val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
-in thy |> Theory.add_path comp_dnam
+in thy |> Sign.add_path comp_dnam
|> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
- |> Theory.parent_path
+ |> Sign.parent_path
end;
end; (* local *)
--- a/src/HOLCF/Tools/domain/domain_extender.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Tue Sep 25 17:06:14 2007 +0200
@@ -105,7 +105,7 @@
val cons''' = map snd eqs''';
fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
- val thy'' = thy''' |> Theory.add_types (map thy_type dtnvs)
+ val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
|> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
@@ -133,9 +133,9 @@
|>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
in
theorems_thy
- |> Theory.add_path (Sign.base_name comp_dnam)
+ |> Sign.add_path (Sign.base_name comp_dnam)
|> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
- |> Theory.parent_path
+ |> Sign.parent_path
end;
val add_domain_i = gen_add_domain Sign.certify_typ;
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Tue Sep 25 17:06:14 2007 +0200
@@ -556,7 +556,7 @@
in
thy
- |> Theory.add_path (Sign.base_name dname)
+ |> Sign.add_path (Sign.base_name dname)
|> (snd o (PureThy.add_thmss (map Thm.no_attributes [
("iso_rews" , iso_rews ),
("exhaust" , [exhaust] ),
@@ -574,7 +574,7 @@
("copy_rews", copy_rews)])))
|> (snd o PureThy.add_thmss
[(("match_rews", mat_rews), [Simplifier.simp_add])])
- |> Theory.parent_path
+ |> Sign.parent_path
|> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
pat_rews @ dist_les @ dist_eqs @ copy_rews)
end; (* let *)
@@ -941,7 +941,7 @@
in pg [] goal tacs end;
end; (* local *)
-in thy |> Theory.add_path comp_dnam
+in thy |> Sign.add_path comp_dnam
|> (snd o (PureThy.add_thmss (map Thm.no_attributes [
("take_rews" , take_rews ),
("take_lemmas", take_lemmas),
@@ -949,7 +949,7 @@
("finite_ind", [finite_ind]),
("ind" , [ind ]),
("coind" , [coind ])])))
- |> Theory.parent_path |> rpair take_rews
+ |> Sign.parent_path |> rpair take_rews
end; (* let *)
end; (* local *)
end; (* struct *)
--- a/src/HOLCF/Tools/pcpodef_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -109,7 +109,7 @@
theory
|> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
(Tactic.rtac (typedef_cpo OF cpo_thms) 1)
- |> Theory.add_path name
+ |> Sign.add_path name
|> PureThy.add_thms
([(("adm_" ^ name, admissible'), []),
(("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),
@@ -118,7 +118,7 @@
(("thelub_" ^ name, typedef_thelub OF cpo_thms), []),
(("compact_" ^ name, typedef_compact OF cpo_thms), [])])
|> snd
- |> Theory.parent_path
+ |> Sign.parent_path
end;
fun make_pcpo UUmem (type_def, less_def, set_def) theory =
@@ -129,7 +129,7 @@
theory
|> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
(Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
- |> Theory.add_path name
+ |> Sign.add_path name
|> PureThy.add_thms
([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
@@ -137,7 +137,7 @@
((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
])
|> snd
- |> Theory.parent_path
+ |> Sign.parent_path
end;
fun pcpodef_result UUmem_admissible theory =
--- a/src/Pure/Proof/extraction.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Sep 25 17:06:14 2007 +0200
@@ -37,7 +37,7 @@
fun add_syntax thy =
thy
|> Theory.copy
- |> Theory.root_path
+ |> Sign.root_path
|> Sign.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
|> Sign.add_consts
[("typeof", "'b::{} => Type", NoSyn),
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Sep 25 17:06:14 2007 +0200
@@ -92,7 +92,7 @@
in
-val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
+val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
end;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Sep 25 17:06:14 2007 +0200
@@ -105,7 +105,7 @@
in
-val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
+val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
end;
--- a/src/Pure/axclass.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/Pure/axclass.ML Tue Sep 25 17:06:14 2007 +0200
@@ -382,9 +382,9 @@
(Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
in
thy
- |> Theory.add_path prefix
+ |> Sign.add_path prefix
|> fold_map add_const consts
- ||> Theory.restore_naming thy
+ ||> Sign.restore_naming thy
|-> (fn cs => mk_axioms cs
#-> (fn axioms_prop => define_class (name, superclasses)
(map fst cs @ other_consts) axioms_prop
--- a/src/ZF/Tools/datatype_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -61,7 +61,7 @@
val rec_base_names = map Sign.base_name rec_names
val big_rec_base_name = space_implode "_" rec_base_names
- val thy_path = thy |> Theory.add_path big_rec_base_name
+ val thy_path = thy |> Sign.add_path big_rec_base_name
val big_rec_name = Sign.intern_const thy_path big_rec_base_name;
@@ -229,13 +229,13 @@
fun add_recursor thy =
if need_recursor then
- thy |> Theory.add_consts_i
+ thy |> Sign.add_consts_i
[(recursor_base_name, recursor_typ, NoSyn)]
|> (snd o PureThy.add_defs_i false [Thm.no_attributes recursor_def])
else thy;
val (con_defs, thy0) = thy_path
- |> Theory.add_consts_i
+ |> Sign.add_consts_i
((case_base_name, case_typ, NoSyn) ::
map #1 (List.concat con_ty_lists))
|> PureThy.add_defs_i false
@@ -244,7 +244,7 @@
List.concat (ListPair.map mk_con_defs
(1 upto npart, con_ty_lists))))
||> add_recursor
- ||> Theory.parent_path
+ ||> Sign.parent_path
val intr_names = map #2 (List.concat con_ty_lists);
val (thy1, ind_result) =
@@ -365,7 +365,7 @@
in
(*Updating theory components: simprules and datatype info*)
- (thy1 |> Theory.add_path big_rec_base_name
+ (thy1 |> Sign.add_path big_rec_base_name
|> PureThy.add_thmss
[(("simps", simps), [Simplifier.simp_add]),
(("", intrs), [Classical.safe_intro NONE]),
@@ -376,7 +376,7 @@
(("free_elims", free_SEs), [])] |> snd
|> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
|> ConstructorsData.map (fold Symtab.update con_pairs)
- |> Theory.parent_path,
+ |> Sign.parent_path,
ind_result,
{con_defs = con_defs,
case_eqns = case_eqns,
--- a/src/ZF/Tools/induct_tacs.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Tue Sep 25 17:06:14 2007 +0200
@@ -157,11 +157,11 @@
in
thy
- |> Theory.add_path (Sign.base_name big_rec_name)
+ |> Sign.add_path (Sign.base_name big_rec_name)
|> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
|> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
|> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
- |> Theory.parent_path
+ |> Sign.parent_path
end;
fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
--- a/src/ZF/Tools/inductive_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/ZF/Tools/inductive_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -172,7 +172,7 @@
(*add definitions of the inductive sets*)
val (_, thy1) =
thy
- |> Theory.add_path big_rec_base_name
+ |> Sign.add_path big_rec_base_name
|> PureThy.add_defs_i false (map Thm.no_attributes axpairs)
@@ -535,7 +535,7 @@
val (intrs'', thy4) =
thy3
|> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
- ||> Theory.parent_path;
+ ||> Sign.parent_path;
in
(thy4,
{defs = defs',
--- a/src/ZF/Tools/numeral_syntax.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML Tue Sep 25 17:06:14 2007 +0200
@@ -100,7 +100,7 @@
val setup =
- (Theory.add_trfuns ([], [("_Int", int_tr)], [], []) #>
- Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
+ (Sign.add_trfuns ([], [("_Int", int_tr)], [], []) #>
+ Sign.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
end;
--- a/src/ZF/Tools/primrec_package.ML Tue Sep 25 15:34:35 2007 +0200
+++ b/src/ZF/Tools/primrec_package.ML Tue Sep 25 17:06:14 2007 +0200
@@ -176,7 +176,7 @@
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
val ([def_thm], thy1) = thy
- |> Theory.add_path (Sign.base_name fname)
+ |> Sign.add_path (Sign.base_name fname)
|> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
@@ -192,7 +192,7 @@
val (_, thy3) =
thy2
|> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
- ||> Theory.parent_path;
+ ||> Sign.parent_path;
in (thy3, eqn_thms') end;
fun add_primrec args thy =