--- a/src/Pure/axclass.ML Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/axclass.ML Wed Mar 17 16:33:00 1999 +0100
@@ -128,7 +128,7 @@
val {sign, hyps, prop, ...} = rep_thm thm;
in
- if not (Sign.subsig (sign, sign_of thy)) then
+ if not (Sign.subsig (sign, Theory.sign_of thy)) then
err "theorem not of same theory"
else if not (null (extra_shyps thm)) orelse not (null hyps) then
err "theorem may not contain hypotheses"
@@ -287,8 +287,8 @@
(* external interfaces *)
-val add_axclass = ext_axclass Sign.intern_class read_axm Attrib.global_attribute;
-val add_axclass_i = ext_axclass (K I) cert_axm (K I);
+val add_axclass = ext_axclass Sign.intern_class Theory.read_axm Attrib.global_attribute;
+val add_axclass_i = ext_axclass (K I) Theory.cert_axm (K I);
@@ -335,14 +335,14 @@
fun prove mk_prop str_of thy sig_prop thms usr_tac =
let
- val sign = sign_of thy;
+ val sign = Theory.sign_of thy;
val goal = Thm.cterm_of sign (mk_prop sig_prop);
val tac = axclass_tac thms THEN (if_none usr_tac all_tac);
in
prove_goalw_cterm [] goal (K [tac])
end
handle ERROR => error ("The error(s) above occurred while trying to prove "
- ^ quote (str_of (sign_of thy, sig_prop)));
+ ^ quote (str_of (Theory.sign_of thy, sig_prop)));
val prove_subclass =
prove mk_classrel (fn (sg, c1_c2) => Sign.str_of_classrel sg c1_c2);
@@ -364,7 +364,7 @@
fun ext_inst_subclass prep_classrel raw_c1_c2 names thms usr_tac thy =
let val c1_c2 = prep_classrel (Theory.sign_of thy) raw_c1_c2 in
message ("Proving class inclusion " ^
- quote (Sign.str_of_classrel (sign_of thy) c1_c2) ^ " ...");
+ quote (Sign.str_of_classrel (Theory.sign_of thy) c1_c2) ^ " ...");
thy |> add_classrel_thms [prove_subclass thy c1_c2 (witnesses thy names thms) usr_tac]
end;
--- a/src/Pure/display.ML Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/display.ML Wed Mar 17 16:33:00 1999 +0100
@@ -121,10 +121,10 @@
(** print theory **)
-val pretty_theory = Sign.pretty_sg o sign_of;
-val pprint_theory = Sign.pprint_sg o sign_of;
+val pretty_theory = Sign.pretty_sg o Theory.sign_of;
+val pprint_theory = Sign.pprint_sg o Theory.sign_of;
-val print_syntax = Syntax.print_syntax o syn_of;
+val print_syntax = Syntax.print_syntax o Theory.syn_of;
(* pretty_name_space *)
@@ -201,7 +201,7 @@
fun print_thy thy =
let
- val {sign, axioms, oracles, ...} = rep_theory thy;
+ val {sign, axioms, oracles, ...} = Theory.rep_theory thy;
val axioms = Symtab.dest axioms;
val oras = map fst (Symtab.dest oracles);
@@ -213,7 +213,7 @@
Pretty.writeln (Pretty.strs ("oracles:" :: oras))
end;
-fun print_theory thy = (print_sign (sign_of thy); print_thy thy);
+fun print_theory thy = (print_sign (Theory.sign_of thy); print_thy thy);
(*also show consts in case of showing types?*)
val show_consts = ref false;
--- a/src/Pure/drule.ML Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/drule.ML Wed Mar 17 16:33:00 1999 +0100
@@ -305,7 +305,7 @@
Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
[ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ] *)
fun assume_ax thy sP =
- let val sign = sign_of thy
+ let val sign = Theory.sign_of thy
val prop = Logic.close_form (term_of (read_cterm sign (sP, propT)))
in forall_elim_vars 0 (assume (cterm_of sign prop)) end;
@@ -420,7 +420,7 @@
(*** Meta-Rewriting Rules ***)
-val proto_sign = sign_of ProtoPure.thy;
+val proto_sign = Theory.sign_of ProtoPure.thy;
fun read_prop s = read_cterm proto_sign (s, propT);
--- a/src/Pure/goals.ML Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/goals.ML Wed Mar 17 16:33:00 1999 +0100
@@ -104,7 +104,7 @@
ref((fn _=> error"No goal has been supplied in subgoal module")
: bool*thm->thm);
-val dummy = trivial(read_cterm (sign_of ProtoPure.thy)
+val dummy = trivial(read_cterm (Theory.sign_of ProtoPure.thy)
("PROP No_goal_has_been_supplied",propT));
(*List of previous goal stacks, for the undo operation. Set by setstate.
@@ -150,14 +150,14 @@
export_thy just goes one up. **)
fun get_top_scope_thms thy =
- let val sc = (Locale.get_scope_sg (sign_of thy))
+ let val sc = (Locale.get_scope_sg (Theory.sign_of thy))
in if (null sc) then (warning "No locale in theory"; [])
else map (#prop o rep_thm) (map #2 (#thms(snd(hd sc))))
end;
fun implies_intr_some_hyps thy A_set th =
let
- val sign = sign_of thy;
+ val sign = Theory.sign_of thy;
val used_As = A_set inter #hyps(rep_thm(th));
val ctl = map (cterm_of sign) used_As
in foldl (fn (x, y) => Thm.implies_intr y x) (th, ctl)
@@ -288,7 +288,7 @@
(*Version taking the goal as a string*)
fun prove_goalw thy rths agoal tacsf =
- let val sign = sign_of thy
+ let val sign = Theory.sign_of thy
val chorn = read_cterm sign (agoal,propT)
in prove_goalw_cterm_general true rths chorn tacsf end
handle ERROR => error (*from read_cterm?*)
@@ -390,7 +390,7 @@
Initial subgoal and premises are rewritten using rths. **)
(*Version taking the goal as a cterm; if you have a term t and theory thy, use
- goalw_cterm rths (cterm_of (sign_of thy) t); *)
+ goalw_cterm rths (cterm_of (Theory.sign_of thy) t); *)
fun agoalw_cterm atomic rths chorn =
let val (prems, st0, mkresult) = prepare_proof atomic rths chorn
in undo_list := [];
@@ -404,7 +404,7 @@
(*Version taking the goal as a string*)
fun agoalw atomic thy rths agoal =
- agoalw_cterm atomic rths (Locale.read_cterm(sign_of thy)(agoal,propT))
+ agoalw_cterm atomic rths (Locale.read_cterm(Theory.sign_of thy)(agoal,propT))
handle ERROR => error (*from type_assign, etc via prepare_proof*)
("The error(s) above occurred for " ^ quote agoal);
--- a/src/Pure/section_utils.ML Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/section_utils.ML Wed Mar 17 16:33:00 1999 +0100
@@ -15,7 +15,7 @@
(*Read an assumption in the given theory*)
-fun assume_read thy a = Thm.assume (read_cterm (sign_of thy) (a,propT));
+fun assume_read thy a = Thm.assume (read_cterm (Theory.sign_of thy) (a,propT));
(*Read a term from string "b", with expected type T*)
fun readtm sign T b =
--- a/src/Pure/tactic.ML Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/tactic.ML Wed Mar 17 16:33:00 1999 +0100
@@ -293,7 +293,7 @@
increment revcut_rl instead.*)
fun make_elim_preserve rl =
let val {maxidx,...} = rep_thm rl
- fun cvar ixn = cterm_of (sign_of ProtoPure.thy) (Var(ixn,propT));
+ fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT));
val revcut_rl' =
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)),
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
--- a/src/Pure/tctical.ML Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/tctical.ML Wed Mar 17 16:33:00 1999 +0100
@@ -357,7 +357,7 @@
(*SELECT_GOAL optimization: replace the conclusion by a variable X,
to avoid copying. Proof states have X==concl as an assuption.*)
-val prop_equals = cterm_of (sign_of ProtoPure.thy)
+val prop_equals = cterm_of (Theory.sign_of ProtoPure.thy)
(Const("==", propT-->propT-->propT));
fun mk_prop_equals(t,u) = capply (capply prop_equals t) u;
@@ -367,7 +367,7 @@
Vars then it returns ct==>ct.*)
fun eq_trivial ct =
- let val xfree = cterm_of (sign_of ProtoPure.thy)
+ let val xfree = cterm_of (Theory.sign_of ProtoPure.thy)
(Free (gensym"EQ_TRIVIAL_", propT))
val ct_eq_x = mk_prop_equals (ct, xfree)
and refl_ct = reflexive ct
@@ -391,7 +391,7 @@
let val np' = nprems_of st'
(*rename the ?A in rev_triv_goal*)
val {maxidx,...} = rep_thm st'
- val ct = cterm_of (sign_of ProtoPure.thy)
+ val ct = cterm_of (Theory.sign_of ProtoPure.thy)
(Var(("A",maxidx+1), propT))
val rev_triv_goal' = instantiate' [] [Some ct] Drule.rev_triv_goal
fun bic th = bicompose false (false, th, np')
--- a/src/Pure/thm.ML Wed Mar 17 16:32:38 1999 +0100
+++ b/src/Pure/thm.ML Wed Mar 17 16:33:00 1999 +0100
@@ -460,7 +460,7 @@
else raise THM ("transfer: not a super theory", 0, [thm])
end;
-val transfer = transfer_sg o sign_of;
+val transfer = transfer_sg o Theory.sign_of;
(*maps object-rule to tpairs*)
fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop);
@@ -627,7 +627,7 @@
(*return additional axioms of this theory node*)
fun axioms_of thy =
map (fn (s, _) => (s, get_axiom thy s))
- (Symtab.dest (#axioms (rep_theory thy)));
+ (Symtab.dest (#axioms (Theory.rep_theory thy)));
(* name and tags -- make proof objects more readable *)
@@ -2296,7 +2296,7 @@
fun invoke_oracle thy raw_name =
let
- val {sign = sg, oracles, ...} = rep_theory thy;
+ val {sign = sg, oracles, ...} = Theory.rep_theory thy;
val name = Sign.intern sg Theory.oracleK raw_name;
val oracle =
(case Symtab.lookup (oracles, name) of