# HG changeset patch
# User wenzelm
# Date 1190732774 -7200
# Node ID 64ed056095683e815a80dc642d3ed46d8d33a3e4
# Parent  e8bba7723858a89bf9a8d90ff0e7cf6cd2924c9a
proper Sign operations instead of Theory aliases;

diff -r e8bba7723858 -r 64ed05609568 src/HOL/Import/import_syntax.ML
--- 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
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Import/proof_kernel.ML
--- 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)=>
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Import/replay.ML
--- 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 = 
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Nominal/nominal_atoms.ML
--- 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;
     
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Nominal/nominal_inductive.ML
--- 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;
 
 
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Nominal/nominal_package.ML
--- 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
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Nominal/nominal_primrec.ML
--- 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 _ =>
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/datatype_abs_proofs.ML
--- 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;
 
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/datatype_aux.ML
--- 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) []);
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/datatype_package.ML
--- 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;
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/datatype_realizer.ML
--- 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,
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/datatype_rep_proofs.ML
--- 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)
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/inductive_realizer.ML
--- 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
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/numeral_syntax.ML
--- 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;
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/primrec_package.ML
--- 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;
 
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/recdef_package.ML
--- 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;
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/record_package.ML
--- 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));
 
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/string_syntax.ML
--- 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')]);
 
diff -r e8bba7723858 -r 64ed05609568 src/HOL/Tools/typedef_package.ML
--- 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,
diff -r e8bba7723858 -r 64ed05609568 src/HOLCF/Tools/domain/domain_axioms.ML
--- 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 *)
diff -r e8bba7723858 -r 64ed05609568 src/HOLCF/Tools/domain/domain_extender.ML
--- 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;
diff -r e8bba7723858 -r 64ed05609568 src/HOLCF/Tools/domain/domain_theorems.ML
--- 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 *)
diff -r e8bba7723858 -r 64ed05609568 src/HOLCF/Tools/pcpodef_package.ML
--- 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 =
diff -r e8bba7723858 -r 64ed05609568 src/Pure/Proof/extraction.ML
--- 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),
diff -r e8bba7723858 -r 64ed05609568 src/Pure/ProofGeneral/proof_general_emacs.ML
--- 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;
 
diff -r e8bba7723858 -r 64ed05609568 src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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;
 
diff -r e8bba7723858 -r 64ed05609568 src/Pure/axclass.ML
--- 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
diff -r e8bba7723858 -r 64ed05609568 src/ZF/Tools/datatype_package.ML
--- 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,
diff -r e8bba7723858 -r 64ed05609568 src/ZF/Tools/induct_tacs.ML
--- 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 =
diff -r e8bba7723858 -r 64ed05609568 src/ZF/Tools/inductive_package.ML
--- 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',
diff -r e8bba7723858 -r 64ed05609568 src/ZF/Tools/numeral_syntax.ML
--- 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;
diff -r e8bba7723858 -r 64ed05609568 src/ZF/Tools/primrec_package.ML
--- 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 =