# HG changeset patch
# User wenzelm
# Date 921684780 -3600
# Node ID 5d58c100ca3fdafa2c8b1582dffc9a7a7806ee03
# Parent  da9c26906f3f0d7a633e9f388a0822903a317b5d
qualify Theory.sign_of etc.;

diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/axclass.ML
--- 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;
 
diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/display.ML
--- 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;
diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/drule.ML
--- 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);
 
diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/goals.ML
--- 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);
 
diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/section_utils.ML
--- 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 = 
diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/tactic.ML
--- 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
diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/tctical.ML
--- 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')
diff -r da9c26906f3f -r 5d58c100ca3f src/Pure/thm.ML
--- 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