# HG changeset patch
# User wenzelm
# Date 921686026 -3600
# Node ID 3d9fd50fcc43b04a4299601dc905613e7e82184e
# Parent  b8dafa978382ff4cc3a1963faf072850aaf00a90
Theory.sign_of;

diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Arith.ML
--- 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
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Integ/Bin.ML
--- 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
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/List.ML
--- 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)
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Prod.ML
--- 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
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Set.ML
--- 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];
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Tools/datatype_abs_proofs.ML
--- 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'
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Tools/datatype_aux.ML
--- 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);
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Tools/datatype_package.ML
--- 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, _) =>
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Tools/datatype_prop.ML
--- 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))));
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Tools/datatype_rep_proofs.ML
--- 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
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Tools/inductive_package.ML
--- 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 *)
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Tools/primrec_package.ML
--- 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;
 
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/Tools/record_package.ML
--- 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
diff -r b8dafa978382 -r 3d9fd50fcc43 src/HOL/simpdata.ML
--- 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 =