--- a/src/HOL/Arith.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Arith.ML Wed Mar 17 16:53:46 1999 +0100
@@ -763,7 +763,7 @@
val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
end;
-fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
+fun mk_cnat n = cterm_of (Theory.sign_of Nat.thy) (HOLogic.mk_nat n);
fun gen_multiply_tac rule k =
if k > 0 then
@@ -807,7 +807,7 @@
(** prepare nat_cancel simprocs **)
-fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
+fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termTVar);
val prep_pats = map prep_pat;
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
@@ -954,7 +954,7 @@
val fast_arith_tac = Fast_Arith.lin_arith_tac;
val nat_arith_simproc_pats =
- map (fn s => Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT))
+ map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT))
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats
--- a/src/HOL/Integ/Bin.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Integ/Bin.ML Wed Mar 17 16:53:46 1999 +0100
@@ -482,7 +482,7 @@
val int_arith_simproc_pats =
- map (fn s => Thm.read_cterm (sign_of Int.thy) (s, HOLogic.boolT))
+ map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
["(m::int) < n","(m::int) <= n", "(m::int) = n"];
val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
--- a/src/HOL/List.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/List.ML Wed Mar 17 16:53:46 1999 +0100
@@ -251,7 +251,7 @@
local
val list_eq_pattern =
- read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
+ Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
(case xs of Const("List.list.[]",_) => cons | _ => last xs)
--- a/src/HOL/Prod.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Prod.ML Wed Mar 17 16:53:46 1999 +0100
@@ -136,7 +136,7 @@
using split_eta a rewrite rule is not general enough, and using
cond_split_eta directly would render some existing proofs very inefficient*)
local
- val split_eta_pat = Thm.read_cterm (sign_of thy)
+ val split_eta_pat = Thm.read_cterm (Theory.sign_of thy)
("split (%x. split (%y. f x y))", HOLogic.termTVar);
val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta);
fun Pair_pat 0 (Bound 0) = true
@@ -431,7 +431,7 @@
(*simplification procedure for unit_eq.
Cannot use this rule directly -- it loops!*)
local
- val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT));
+ val unit_pat = Thm.cterm_of (Theory.sign_of thy) (Free ("x", HOLogic.unitT));
val unit_meta_eq = standard (mk_meta_eq unit_eq);
fun proc _ _ t =
if HOLogic.is_unit t then None
--- a/src/HOL/Set.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Set.ML Wed Mar 17 16:53:46 1999 +0100
@@ -656,9 +656,9 @@
(*Split ifs on either side of the membership relation.
Not for Addsimps -- can cause goals to blow up!*)
bind_thm ("split_if_mem1",
- read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
+ read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
bind_thm ("split_if_mem2",
- read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
+ read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
split_if_mem1, split_if_mem2];
--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Mar 17 16:53:46 1999 +0100
@@ -52,7 +52,7 @@
open DatatypeAux;
-val thin = read_instantiate_sg (sign_of Set.thy) [("V", "?X : ?Y")] thin_rl;
+val thin = read_instantiate_sg (Theory.sign_of Set.thy) [("V", "?X : ?Y")] thin_rl;
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
@@ -75,7 +75,7 @@
val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", 0), T), Bound 0) $
Var (("P", 0), HOLogic.boolT))
val insts = take (i, dummyPs) @ (P::(drop (i + 1, dummyPs)));
- val cert = cterm_of (sign_of thy);
+ val cert = cterm_of (Theory.sign_of thy);
val insts' = (map cert induct_Ps) ~~ (map cert insts);
val induct' = refl RS ((nth_elem (i,
split_conj_thm (cterm_instantiate insts' induct))) RSN (2, rev_mp))
@@ -112,7 +112,7 @@
val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
val big_rec_name' = big_name ^ "_rec_set";
- val rec_set_names = map (Sign.full_name (sign_of thy0))
+ val rec_set_names = map (Sign.full_name (Theory.sign_of thy0))
(if length descr' = 1 then [big_rec_name'] else
(map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
(1 upto (length descr'))));
@@ -221,7 +221,7 @@
absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod
(mk_Free "x" T1 i, Free ("y", T2)), set_t)))
(rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
- val cert = cterm_of (sign_of thy1)
+ val cert = cterm_of (Theory.sign_of thy1)
val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
val induct' = cterm_instantiate ((map cert induct_Ps) ~~
@@ -239,7 +239,7 @@
(* define primrec combinators *)
val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
- val reccomb_names = map (Sign.full_name (sign_of thy1))
+ val reccomb_names = map (Sign.full_name (Theory.sign_of thy1))
(if length descr' = 1 then [big_reccomb_name] else
(map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
@@ -266,7 +266,7 @@
val _ = message "Proving characteristic theorems for primrec combinators..."
val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
- (cterm_of (sign_of thy2) t) (fn _ =>
+ (cterm_of (Theory.sign_of thy2) t) (fn _ =>
[rtac select1_equality 1,
resolve_tac rec_unique_thms 1,
resolve_tac rec_intrs 1,
@@ -302,7 +302,7 @@
end) constrs) descr';
val case_names = map (fn s =>
- Sign.full_name (sign_of thy1) (s ^ "_case")) new_type_names;
+ Sign.full_name (Theory.sign_of thy1) (s ^ "_case")) new_type_names;
(* define case combinators via primrec combinators *)
@@ -338,7 +338,7 @@
(take (length newTs, reccomb_names)));
val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
- (map mk_meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
+ (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t)
(fn _ => [rtac refl 1])))
(DatatypeProp.make_cases new_type_names descr sorts thy2);
@@ -374,8 +374,8 @@
val mk_abs = foldr (fn (T, t') => Abs ("x", T, t'));
val fs = map mk_abs (Tss ~~ ts);
val fTs = map (fn Ts => Ts ---> HOLogic.natT) Tss;
- val ord_name = Sign.full_name (sign_of thy) (tname ^ "_ord");
- val case_name = Sign.intern_const (sign_of thy) (tname ^ "_case");
+ val ord_name = Sign.full_name (Theory.sign_of thy) (tname ^ "_ord");
+ val case_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_case");
val ordT = T --> HOLogic.natT;
val caseT = fTs ---> ordT;
val defpair = (tname ^ "_ord_def", Logic.mk_equals
@@ -395,7 +395,7 @@
fun prove_distinct_thms _ [] = []
| prove_distinct_thms dist_rewrites' (t::_::ts) =
let
- val dist_thm = prove_goalw_cterm [] (cterm_of (sign_of thy2) t) (fn _ =>
+ val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy2) t) (fn _ =>
[simp_tac (HOL_ss addsimps dist_rewrites') 1])
in dist_thm::(standard (dist_thm RS not_sym))::
(prove_distinct_thms dist_rewrites' ts)
@@ -409,7 +409,7 @@
let
val t::ts' = rev ts;
val (_ $ (_ $ (_ $ (f $ _) $ _))) = hd (Logic.strip_imp_prems t);
- val cert = cterm_of (sign_of thy2);
+ val cert = cterm_of (Theory.sign_of thy2);
val distinct_lemma' = cterm_instantiate
[(cert distinct_f, cert f)] distinct_lemma;
val rewrites = ord_defs @ (map mk_meta_eq case_thms)
@@ -439,7 +439,7 @@
fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
exhaustion), case_thms'), T) =
let
- val cert = cterm_of (sign_of thy);
+ val cert = cterm_of (Theory.sign_of thy);
val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
val exhaustion' = cterm_instantiate
[(cert lhs, cert (Free ("x", T)))] exhaustion;
@@ -475,9 +475,9 @@
val recTs = get_rec_types descr' sorts;
val big_size_name = space_implode "_" new_type_names ^ "_size";
- val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy1))) "size";
+ val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy1))) "size";
val size_names = replicate (length (hd descr)) size_name @
- map (Sign.full_name (sign_of thy1))
+ map (Sign.full_name (Theory.sign_of thy1))
(if length (flat (tl descr)) = 1 then [big_size_name] else
map (fn i => big_size_name ^ "_" ^ string_of_int i)
(1 upto length (flat (tl descr))));
@@ -513,7 +513,7 @@
val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
val size_thms = map (fn t => prove_goalw_cterm rewrites
- (cterm_of (sign_of thy') t) (fn _ => [rtac refl 1]))
+ (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1]))
(DatatypeProp.make_size new_type_names descr sorts thy')
in
@@ -536,7 +536,7 @@
hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
| tac i n = rtac disjI2 i THEN tac i (n - 1)
in
- prove_goalw_cterm [] (cterm_of (sign_of thy) t) (fn _ =>
+ prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ =>
[rtac allI 1,
exh_tac (K exhaustion) 1,
ALLGOALS (fn i => tac i (i-1))])
@@ -555,7 +555,7 @@
let
val (Const ("==>", _) $ tm $ _) = t;
val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
- val cert = cterm_of (sign_of thy);
+ val cert = cterm_of (Theory.sign_of thy);
val nchotomy' = nchotomy RS spec;
val nchotomy'' = cterm_instantiate
[(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
--- a/src/HOL/Tools/datatype_aux.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Wed Mar 17 16:53:46 1999 +0100
@@ -68,7 +68,7 @@
fun foldl1 f (x::xs) = foldl f (x, xs);
fun get_thy name thy = find_first
- (equal name o Sign.name_of o sign_of) (ancestors_of thy);
+ (equal name o Sign.name_of o Theory.sign_of) (Theory.ancestors_of thy);
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;
@@ -113,7 +113,7 @@
None => let val [Free (s, T)] = add_term_frees (t2, [])
in absfree (s, T, t2) end
| Some (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
- val cert = cterm_of (sign_of_thm st);
+ val cert = cterm_of (Thm.sign_of_thm st);
val Ps = map (cert o head_of o snd o getP) ts;
val indrule' = cterm_instantiate (Ps ~~
(map (cert o abstr o getP) ts')) indrule
@@ -125,7 +125,7 @@
fun exh_tac exh_thm_of i state =
let
- val sg = sign_of_thm state;
+ val sg = Thm.sign_of_thm state;
val prem = nth_elem (i - 1, prems_of state);
val params = Logic.strip_params prem;
val (_, Type (tname, _)) = hd (rev params);
--- a/src/HOL/Tools/datatype_package.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Mar 17 16:53:46 1999 +0100
@@ -111,7 +111,7 @@
Some info => info
| None => error ("Unknown datatype " ^ quote name));
-val datatype_info = datatype_info_sg o sign_of;
+val datatype_info = datatype_info_sg o Theory.sign_of;
fun constrs_of thy tname =
let
@@ -119,14 +119,14 @@
val (_, _, constrs) = the (assoc (descr, index))
in
Some (map (fn (cname, _) =>
- Const (cname, the (Sign.const_type (sign_of thy) cname))) constrs)
+ Const (cname, the (Sign.const_type (Theory.sign_of thy) cname))) constrs)
end handle _ => None;
fun case_const_of thy tname =
let
val {case_name, ...} = datatype_info thy tname;
in
- Some (Const (case_name, the (Sign.const_type (sign_of thy) case_name)))
+ Some (Const (case_name, the (Sign.const_type (Theory.sign_of thy) case_name)))
end handle _ => None;
fun find_tname var Bi =
@@ -340,8 +340,8 @@
(case_names ~~ newTs ~~ case_fn_Ts)) |>
Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr);
- val reccomb_names' = map (Sign.intern_const (sign_of thy2')) reccomb_names;
- val case_names' = map (Sign.intern_const (sign_of thy2')) case_names;
+ val reccomb_names' = map (Sign.intern_const (Theory.sign_of thy2')) reccomb_names;
+ val case_names' = map (Sign.intern_const (Theory.sign_of thy2')) case_names;
val thy2 = thy2' |>
@@ -501,7 +501,7 @@
|> app_thmss raw_distinct
|> apfst (app_thmss raw_inject)
|> apfst (apfst (app_thm raw_induction));
- val sign = sign_of thy1;
+ val sign = Theory.sign_of thy1;
val induction' = freezeT induction;
@@ -549,7 +549,7 @@
val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
[descr] sorts nchotomys case_thms thy6;
val (thy8, size_thms) =
- if exists (equal "Arith") (Sign.stamp_names_of (sign_of thy7)) then
+ if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy7)) then
DatatypeAbsProofs.prove_size_thms false new_type_names
[descr] sorts reccomb_names rec_thms thy7
else (thy7, []);
@@ -600,7 +600,7 @@
Theory.add_types (map (fn (tvs, tname, mx, _) =>
(tname, length tvs, mx)) dts);
- val sign = sign_of tmp_thy;
+ val sign = Theory.sign_of tmp_thy;
val (tyvars, _, _, _)::_ = dts;
val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
--- a/src/HOL/Tools/datatype_prop.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Tools/datatype_prop.ML Wed Mar 17 16:53:46 1999 +0100
@@ -162,7 +162,7 @@
fun make_primrecs new_type_names descr sorts thy =
let
- val sign = sign_of thy;
+ val sign = Theory.sign_of thy;
val descr' = flat descr;
val recTs = get_rec_types descr' sorts;
@@ -229,7 +229,7 @@
in Ts ---> T' end) constrs) (hd descr);
val case_names = map (fn s =>
- Sign.intern_const (sign_of thy) (s ^ "_case")) new_type_names
+ Sign.intern_const (Theory.sign_of thy) (s ^ "_case")) new_type_names
in
map (fn ((name, Ts), T) => list_comb
(Const (name, Ts @ [T] ---> T'),
@@ -296,7 +296,7 @@
fun make_distincts_2 T tname i constrs =
let
- val ord_name = Sign.intern_const (sign_of thy) (tname ^ "_ord");
+ val ord_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_ord");
val ord_t = Const (ord_name, T --> HOLogic.natT)
in (case constrs of
@@ -403,9 +403,9 @@
val recTs = get_rec_types descr' sorts;
val big_size_name = space_implode "_" new_type_names ^ "_size";
- val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy))) "size";
+ val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy))) "size";
val size_names = replicate (length (hd descr)) size_name @
- map (Sign.intern_const (sign_of thy))
+ map (Sign.intern_const (Theory.sign_of thy))
(if length (flat (tl descr)) = 1 then [big_size_name] else
map (fn i => big_size_name ^ "_" ^ string_of_int i)
(1 upto length (flat (tl descr))));
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Mar 17 16:53:46 1999 +0100
@@ -30,10 +30,10 @@
(* figure out internal names *)
-val image_name = Sign.intern_const (sign_of Set.thy) "op ``";
-val UNIV_name = Sign.intern_const (sign_of Set.thy) "UNIV";
-val inj_on_name = Sign.intern_const (sign_of Fun.thy) "inj_on";
-val inv_name = Sign.intern_const (sign_of Fun.thy) "inv";
+val image_name = Sign.intern_const (Theory.sign_of Set.thy) "op ``";
+val UNIV_name = Sign.intern_const (Theory.sign_of Set.thy) "UNIV";
+val inj_on_name = Sign.intern_const (Theory.sign_of Fun.thy) "inj_on";
+val inv_name = Sign.intern_const (Theory.sign_of Fun.thy) "inv";
fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
#exhaustion (the (Symtab.lookup (dt_info, tname)));
@@ -44,9 +44,9 @@
new_type_names descr sorts types_syntax constr_syntax thy =
let
val Univ_thy = the (get_thy "Univ" thy);
- val node_name = Sign.intern_tycon (sign_of Univ_thy) "node";
+ val node_name = Sign.intern_tycon (Theory.sign_of Univ_thy) "node";
val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name] =
- map (Sign.intern_const (sign_of Univ_thy))
+ map (Sign.intern_const (Theory.sign_of Univ_thy))
["In0", "In1", "Scons", "Leaf", "Numb"];
val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
In0_not_In1, In1_not_In0] = map (get_thm Univ_thy)
@@ -58,7 +58,7 @@
val big_name = space_implode "_" new_type_names;
val thy1 = add_path flat_names big_name thy;
val big_rec_name = big_name ^ "_rep_set";
- val rep_set_names = map (Sign.full_name (sign_of thy1))
+ val rep_set_names = map (Sign.full_name (Theory.sign_of thy1))
(if length descr' = 1 then [big_rec_name] else
(map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
(1 upto (length descr'))));
@@ -153,8 +153,8 @@
val rep_names = map (curry op ^ "Rep_") new_type_names;
val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
(1 upto (length (flat (tl descr))));
- val all_rep_names = map (Sign.intern_const (sign_of thy3)) rep_names @
- map (Sign.full_name (sign_of thy3)) rep_names';
+ val all_rep_names = map (Sign.intern_const (Theory.sign_of thy3)) rep_names @
+ map (Sign.full_name (Theory.sign_of thy3)) rep_names';
(* isomorphism declarations *)
@@ -176,8 +176,8 @@
val (_, l_args, r_args) = foldr constr_arg (cargs, (1, [], []));
val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
- val abs_name = Sign.intern_const (sign_of thy) ("Abs_" ^ tname);
- val rep_name = Sign.intern_const (sign_of thy) ("Rep_" ^ tname);
+ val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
+ val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
val lhs = list_comb (Const (cname, constrT), l_args);
val rhs = mk_univ_inj r_args n i;
val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
@@ -197,7 +197,7 @@
((((_, (_, _, constrs)), tname), T), constr_syntax)) =
let
val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
- val sg = sign_of thy;
+ val sg = Theory.sign_of thy;
val rep_const = cterm_of sg
(Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT));
val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
@@ -231,7 +231,7 @@
fun prove_newT_iso_inj_thm (((s, (thm1, thm2, _)), T), rep_set_name) =
let
- val sg = sign_of thy4;
+ val sg = Theory.sign_of thy4;
val RepT = T --> Univ_elT;
val Rep_name = Sign.intern_const sg ("Rep_" ^ s);
val AbsT = Univ_elT --> T;
@@ -331,7 +331,7 @@
val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
- (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
+ (cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
in (thy', char_thms' @ char_thms) end;
@@ -361,7 +361,7 @@
val iso_thms = if length descr = 1 then [] else
drop (length newTs, split_conj_thm
- (prove_goalw_cterm [] (cterm_of (sign_of thy5) iso_t) (fn _ =>
+ (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
[indtac rep_induct 1,
REPEAT (rtac TrueI 1),
REPEAT (EVERY
@@ -397,7 +397,7 @@
val rewrites = map mk_meta_eq iso_char_thms;
val inj_thms' = map (fn r => r RS injD) inj_thms;
- val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
+ val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
(HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
[indtac induction 1,
REPEAT (EVERY
@@ -421,7 +421,7 @@
val elem_thm =
prove_goalw_cterm []
- (cterm_of (sign_of thy5)
+ (cterm_of (Theory.sign_of thy5)
(HOLogic.mk_Trueprop (mk_conj ind_concl2)))
(fn _ =>
[indtac induction 1,
@@ -447,7 +447,7 @@
let
val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
- in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
+ in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
[resolve_tac inj_thms 1,
rewrite_goals_tac rewrites,
rtac refl 1,
@@ -473,7 +473,7 @@
let val inj_thms = Scons_inject::(map make_elim
((map (fn r => r RS injD) iso_inj_thms) @
[In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject]))
- in prove_goalw_cterm [] (cterm_of (sign_of thy5) t) (fn _ =>
+ in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
[rtac iffI 1,
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
dresolve_tac rep_congs 1, dtac box_equals 1,
@@ -504,7 +504,7 @@
mk_Free "x" T i;
val Abs_t = if i < length newTs then
- Const (Sign.intern_const (sign_of thy6)
+ Const (Sign.intern_const (Theory.sign_of thy6)
("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT --> T)
else Const (inv_name, [T --> Univ_elT, Univ_elT] ---> T) $
Const (nth_elem (i, all_rep_names), T --> Univ_elT)
@@ -518,7 +518,7 @@
val (indrule_lemma_prems, indrule_lemma_concls) =
foldl mk_indrule_lemma (([], []), (descr' ~~ recTs));
- val cert = cterm_of (sign_of thy6);
+ val cert = cterm_of (Theory.sign_of thy6);
val indrule_lemma = prove_goalw_cterm [] (cert
(Logic.mk_implies
--- a/src/HOL/Tools/inductive_package.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Tools/inductive_package.ML Wed Mar 17 16:53:46 1999 +0100
@@ -63,8 +63,8 @@
(*For simplifying the elimination rule*)
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
-val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op -``";
-val mono_name = Sign.intern_const (sign_of Ord.thy) "mono";
+val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
+val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
(* make injections needed in mutually recursive definitions *)
@@ -225,7 +225,7 @@
let
val _ = message " Proving monotonicity...";
- val mono = prove_goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop
+ val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
(Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
(fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)])
@@ -245,7 +245,7 @@
| select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
- (cterm_of (sign_of thy) intr) (fn prems =>
+ (cterm_of (Theory.sign_of thy) intr) (fn prems =>
[(*insert prems and underlying sets*)
cut_facts_tac prems 1,
stac unfold 1,
@@ -272,7 +272,7 @@
map make_elim [Inl_inject, Inr_inject];
val elims = map (fn t => prove_goalw_cterm rec_sets_defs
- (cterm_of (sign_of thy) t) (fn prems =>
+ (cterm_of (Theory.sign_of thy) t) (fn prems =>
[cut_facts_tac [hd prems] 1,
dtac (unfold RS subst) 1,
REPEAT (FIRSTGOAL (eresolve_tac rules1)),
@@ -300,7 +300,7 @@
(*String s should have the form t:Si where Si is an inductive set*)
fun mk_cases elims s =
- let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT))
+ let val prem = assume (read_cterm (Thm.sign_of_thm (hd elims)) (s, propT))
fun mk_elim rl = rule_by_tactic (con_elim_tac (simpset())) (prem RS rl)
|> standard
in case find_first is_some (map (try mk_elim) elims) of
@@ -315,7 +315,7 @@
let
val _ = message " Proving the induction rule...";
- val sign = sign_of thy;
+ val sign = Theory.sign_of thy;
val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
@@ -387,8 +387,8 @@
val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
val setT = HOLogic.mk_setT sumT;
- val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp"
- else Sign.intern_const (sign_of Lfp.thy) "lfp";
+ val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
+ else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
val used = foldr add_term_names (intr_ts, []);
val [sname, xname] = variantlist (["S", "x"], used);
@@ -421,7 +421,7 @@
(* add definiton of recursive sets to theory *)
val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
- val full_rec_name = Sign.full_name (sign_of thy) rec_name;
+ val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
val rec_const = list_comb
(Const (full_rec_name, paramTs ---> setT), params);
@@ -538,7 +538,7 @@
val _ = Theory.requires thy "Inductive"
((if coind then "co" else "") ^ "inductive definitions");
- val sign = sign_of thy;
+ val sign = Theory.sign_of thy;
(*parameters should agree for all mutually recursive components*)
val (_, params) = strip_comb (hd cs);
@@ -566,9 +566,9 @@
fun add_inductive verbose coind c_strings intr_strings monos con_defs thy =
let
- val sign = sign_of thy;
- val cs = map (readtm (sign_of thy) HOLogic.termTVar) c_strings;
- val intr_ts = map (readtm (sign_of thy) propT) intr_strings;
+ val sign = Theory.sign_of thy;
+ val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings;
+ val intr_ts = map (readtm (Theory.sign_of thy) propT) intr_strings;
(* the following code ensures that each recursive set *)
(* always has the same type in all introduction rules *)
--- a/src/HOL/Tools/primrec_package.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Mar 17 16:53:46 1999 +0100
@@ -193,9 +193,7 @@
fs @ map Bound (0 ::(length ls downto 1))));
val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
Logic.mk_equals (Const (fname, dummyT), rhs))
- in
- inferT_axm sign defpair
- end;
+ in Theory.inferT_axm sign defpair end;
(* find datatypes which contain all datatypes in tnames' *)
@@ -212,7 +210,7 @@
fun add_primrec_i alt_name eqns_atts thy =
let
val (eqns, atts) = split_list eqns_atts;
- val sg = sign_of thy;
+ val sg = Theory.sign_of thy;
val dt_info = DatatypePackage.get_datatypes thy;
val rec_eqns = foldr (process_eqn sg) (map snd eqns, []);
val tnames = distinct (map (#1 o snd) rec_eqns);
@@ -242,7 +240,7 @@
val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
val _ = writeln ("Proving equations for primrec function(s)\n" ^
commas_quote names1 ^ " ...");
- val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
+ val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
(fn _ => [rtac refl 1])) eqns;
val simps = char_thms;
val thy'' =
@@ -254,7 +252,7 @@
fun read_eqn thy ((name, s), srcs) =
- ((name, readtm (sign_of thy) propT s), map (Attrib.global_attribute thy) srcs);
+ ((name, readtm (Theory.sign_of thy) propT s), map (Attrib.global_attribute thy) srcs);
fun add_primrec alt_name eqns thy = add_primrec_i alt_name (map (read_eqn thy) eqns) thy;
--- a/src/HOL/Tools/record_package.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/Tools/record_package.ML Wed Mar 17 16:53:46 1999 +0100
@@ -456,7 +456,7 @@
fun field_type_def ((thy, simps), (name, tname, vs, T, U)) =
let
- val full = Sign.full_name (sign_of thy);
+ val full = Sign.full_name (Theory.sign_of thy);
val (thy', {simps = simps', ...}) =
thy
|> setmp DatatypePackage.quiet_mode true
--- a/src/HOL/simpdata.ML Wed Mar 17 16:53:32 1999 +0100
+++ b/src/HOL/simpdata.ML Wed Mar 17 16:53:46 1999 +0100
@@ -315,10 +315,10 @@
local
val ex_pattern =
- read_cterm (sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
+ Thm.read_cterm (Theory.sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
val all_pattern =
- read_cterm (sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
+ Thm.read_cterm (Theory.sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
in
val defEX_regroup =