proper Sign operations instead of Theory aliases;
authorwenzelm
Tue Sep 25 17:06:14 2007 +0200 (2007-09-25)
changeset 2471264ed05609568
parent 24711 e8bba7723858
child 24713 8b3b6d09ef40
proper Sign operations instead of Theory aliases;
src/HOL/Import/import_syntax.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/numeral_syntax.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/string_syntax.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/Tools/domain/domain_axioms.ML
src/HOLCF/Tools/domain/domain_extender.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/HOLCF/Tools/pcpodef_package.ML
src/Pure/Proof/extraction.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/axclass.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/numeral_syntax.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Import/import_syntax.ML	Tue Sep 25 15:34:35 2007 +0200
     1.2 +++ b/src/HOL/Import/import_syntax.ML	Tue Sep 25 17:06:14 2007 +0200
     1.3 @@ -45,7 +45,7 @@
     1.4  val import_theory = P.name >> (fn thyname =>
     1.5  			       fn thy =>
     1.6  				  thy |> set_generating_thy thyname
     1.7 -				      |> Theory.add_path thyname
     1.8 +				      |> Sign.add_path thyname
     1.9  				      |> add_dump (";setup_theory " ^ thyname))
    1.10  
    1.11  fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I)
    1.12 @@ -80,7 +80,7 @@
    1.13  		    |> replay 
    1.14  		    |> clear_used_names
    1.15  		    |> export_hol4_pending
    1.16 -		    |> Theory.parent_path
    1.17 +		    |> Sign.parent_path
    1.18  		    |> dump_import_thy thyname
    1.19  		    |> add_dump ";end_setup"
    1.20  	    end) toks
    1.21 @@ -175,7 +175,7 @@
    1.22  	fun apply [] thy = thy
    1.23  	  | apply (f::fs) thy = apply fs (f thy)
    1.24      in
    1.25 -	apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
    1.26 +	apply (set_replaying_thy s::Sign.add_path s::(fst (importP token_list)))
    1.27      end
    1.28  
    1.29  fun create_int_thms thyname thy =
    1.30 @@ -215,7 +215,7 @@
    1.31  		thy |> set_segment thyname segname
    1.32  		    |> clear_import_thy
    1.33  		    |> clear_int_thms
    1.34 -		    |> Theory.parent_path
    1.35 +		    |> Sign.parent_path
    1.36  	    end) toks
    1.37  
    1.38  val set_dump  = P.string -- P.string   >> setup_dump
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Sep 25 15:34:35 2007 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Tue Sep 25 17:06:14 2007 +0200
     2.3 @@ -1928,7 +1928,7 @@
     2.4  	val csyn = mk_syn thy constname
     2.5  	val thy1 = case HOL4DefThy.get thy of
     2.6  		       Replaying _ => thy
     2.7 -		     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Theory.add_consts_i [(constname,ctype,csyn)] thy)
     2.8 +		     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy)
     2.9  	val eq = mk_defeq constname rhs' thy1
    2.10  	val (thms, thy2) = PureThy.add_defs_i false [((thmname,eq),[])] thy1
    2.11  	val _ = ImportRecorder.add_defs thmname eq
    2.12 @@ -2019,7 +2019,7 @@
    2.13  			       val thy' = add_dump str thy
    2.14  			       val _ = ImportRecorder.add_consts consts
    2.15  			   in
    2.16 -			       Theory.add_consts_i consts thy'
    2.17 +			       Sign.add_consts_i consts thy'
    2.18  			   end
    2.19  
    2.20  	    val thy1 = foldr (fn(name,thy)=>
     3.1 --- a/src/HOL/Import/replay.ML	Tue Sep 25 15:34:35 2007 +0200
     3.2 +++ b/src/HOL/Import/replay.ML	Tue Sep 25 17:06:14 2007 +0200
     3.3 @@ -334,7 +334,7 @@
     3.4  	    add_hol4_mapping thyname thmname isaname thy
     3.5  	  | delta (Hol_pending (thyname, thmname, th)) thy = 
     3.6  	    add_hol4_pending thyname thmname ([], th_of thy th) thy
     3.7 -	  | delta (Consts cs) thy = Theory.add_consts_i cs thy
     3.8 +	  | delta (Consts cs) thy = Sign.add_consts_i cs thy
     3.9  	  | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
    3.10  	    add_hol4_const_mapping thyname constname true fullcname thy
    3.11  	  | delta (Hol_move (fullname, moved_thmname)) thy = 
     4.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Tue Sep 25 15:34:35 2007 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Sep 25 17:06:14 2007 +0200
     4.3 @@ -163,7 +163,7 @@
     4.4                      cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
     4.5          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
     4.6        in
     4.7 -        thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
     4.8 +        thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
     4.9              |> PureThy.add_defs_unchecked_i true [((name, def2),[])]
    4.10              |> snd
    4.11              |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
    4.12 @@ -193,7 +193,7 @@
    4.13                     (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
    4.14                      Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
    4.15        in
    4.16 -        thy |> Theory.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
    4.17 +        thy |> Sign.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
    4.18              |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
    4.19        end) ak_names_types thy3;
    4.20      
     5.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Sep 25 15:34:35 2007 +0200
     5.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Sep 25 17:06:14 2007 +0200
     5.3 @@ -419,7 +419,7 @@
     5.4            else (strong_raw_induct RSN (2, rev_mp),
     5.5              [ind_case_names, RuleCases.consumes 1]);
     5.6          val ([strong_induct'], thy') = thy |>
     5.7 -          Theory.add_path rec_name |>
     5.8 +          Sign.add_path rec_name |>
     5.9            PureThy.add_thms [(("strong_induct", #1 strong_induct), #2 strong_induct)];
    5.10          val strong_inducts =
    5.11            ProjectRule.projects ctxt (1 upto length names) strong_induct'
    5.12 @@ -427,7 +427,7 @@
    5.13          thy' |>
    5.14          PureThy.add_thmss [(("strong_inducts", strong_inducts),
    5.15            [ind_case_names, RuleCases.consumes 1])] |> snd |>
    5.16 -        Theory.parent_path
    5.17 +        Sign.parent_path
    5.18        end))
    5.19        (map (map (rulify_term thy #> rpair [])) vc_compat)
    5.20    end;
    5.21 @@ -506,9 +506,9 @@
    5.22        end) atoms
    5.23    in
    5.24      fold (fn (name, ths) =>
    5.25 -      Theory.add_path (Sign.base_name name) #>
    5.26 +      Sign.add_path (Sign.base_name name) #>
    5.27        PureThy.add_thmss [(("eqvt", ths), [NominalThmDecls.eqvt_add])] #> snd #>
    5.28 -      Theory.parent_path) (names ~~ transp thss) thy
    5.29 +      Sign.parent_path) (names ~~ transp thss) thy
    5.30    end;
    5.31  
    5.32  
     6.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Sep 25 15:34:35 2007 +0200
     6.2 +++ b/src/HOL/Nominal/nominal_package.ML	Tue Sep 25 17:06:14 2007 +0200
     6.3 @@ -235,7 +235,7 @@
     6.4  
     6.5      val tmp_thy = thy |>
     6.6        Theory.copy |>
     6.7 -      Theory.add_types (map (fn (tvs, tname, mx, _) =>
     6.8 +      Sign.add_types (map (fn (tvs, tname, mx, _) =>
     6.9          (tname, length tvs, mx)) dts);
    6.10  
    6.11      val atoms = atoms_of thy;
    6.12 @@ -330,7 +330,7 @@
    6.13        end) descr);
    6.14  
    6.15      val (perm_simps, thy2) = thy1 |>
    6.16 -      Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
    6.17 +      Sign.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
    6.18          (List.drop (perm_names_types, length new_type_names))) |>
    6.19        PrimrecPackage.add_primrec_unchecked_i "" perm_eqs;
    6.20  
    6.21 @@ -820,7 +820,7 @@
    6.22            (Const (rep_name, T --> T') $ lhs, rhs));
    6.23          val def_name = (Sign.base_name cname) ^ "_def";
    6.24          val ([def_thm], thy') = thy |>
    6.25 -          Theory.add_consts_i [(cname', constrT, mx)] |>
    6.26 +          Sign.add_consts_i [(cname', constrT, mx)] |>
    6.27            (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
    6.28        in (thy', defs @ [def_thm], eqns @ [eqn]) end;
    6.29  
    6.30 @@ -831,7 +831,7 @@
    6.31            (Const (Sign.intern_const thy ("Rep_" ^ tname), T --> T'));
    6.32          val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    6.33          val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T')
    6.34 -          ((Theory.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
    6.35 +          ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax)
    6.36        in
    6.37          (parent_path flat_names thy', defs', eqns @ [eqns'], dist_lemmas @ [dist])
    6.38        end;
    6.39 @@ -1128,10 +1128,10 @@
    6.40      val simp_eqvt_atts = replicate (length new_type_names) [Simplifier.simp_add, NominalThmDecls.eqvt_add];
    6.41   
    6.42      val (_, thy9) = thy8 |>
    6.43 -      Theory.add_path big_name |>
    6.44 +      Sign.add_path big_name |>
    6.45        PureThy.add_thms [(("weak_induct", dt_induct), [case_names_induct])] ||>>
    6.46        PureThy.add_thmss [(("weak_inducts", projections dt_induct), [case_names_induct])] ||>
    6.47 -      Theory.parent_path ||>>
    6.48 +      Sign.parent_path ||>>
    6.49        DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
    6.50        DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
    6.51        DatatypeAux.store_thmss_atts "perm" new_type_names simp_eqvt_atts perm_simps' ||>>
    6.52 @@ -1409,7 +1409,7 @@
    6.53              (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
    6.54  
    6.55      val (_, thy10) = thy9 |>
    6.56 -      Theory.add_path big_name |>
    6.57 +      Sign.add_path big_name |>
    6.58        PureThy.add_thms [(("induct'", induct_aux), [])] ||>>
    6.59        PureThy.add_thms [(("induct", induct), [case_names_induct])] ||>>
    6.60        PureThy.add_thmss [(("inducts", projections induct), [case_names_induct])];
    6.61 @@ -2022,7 +2022,7 @@
    6.62  
    6.63      val (reccomb_defs, thy12) =
    6.64        thy11
    6.65 -      |> Theory.add_consts_i (map (fn ((name, T), T') =>
    6.66 +      |> Sign.add_consts_i (map (fn ((name, T), T') =>
    6.67            (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
    6.68            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    6.69        |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    6.70 @@ -2067,7 +2067,7 @@
    6.71           (("rec_fresh", List.concat rec_fresh_thms), []),
    6.72           (("rec_unique", map standard rec_unique_thms), []),
    6.73           (("recs", rec_thms), [])] ||>
    6.74 -      Theory.parent_path ||>
    6.75 +      Sign.parent_path ||>
    6.76        map_nominal_datatypes (fold Symtab.update dt_infos);
    6.77  
    6.78    in
     7.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Sep 25 15:34:35 2007 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Sep 25 17:06:14 2007 +0200
     7.3 @@ -275,7 +275,7 @@
     7.4        if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
     7.5      val (defs_thms', thy') =
     7.6        thy
     7.7 -      |> Theory.add_path primrec_name
     7.8 +      |> Sign.add_path primrec_name
     7.9        |> fold_map def (map (fn ((name, t), _) => ((name, []), t)) defs');
    7.10      val cert = cterm_of thy';
    7.11  
    7.12 @@ -369,7 +369,7 @@
    7.13             thy'
    7.14             |> note (("simps", [Simplifier.simp_add]), simps'')
    7.15             |> snd
    7.16 -           |> Theory.parent_path
    7.17 +           |> Sign.parent_path
    7.18           end))
    7.19        [goals] |>
    7.20      Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
     8.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 25 15:34:35 2007 +0200
     8.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Sep 25 17:06:14 2007 +0200
     8.3 @@ -234,7 +234,7 @@
     8.4  
     8.5      val (reccomb_defs, thy2) =
     8.6        thy1
     8.7 -      |> Theory.add_consts_i (map (fn ((name, T), T') =>
     8.8 +      |> Sign.add_consts_i (map (fn ((name, T), T') =>
     8.9            (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
    8.10            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    8.11        |> (PureThy.add_defs_i false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    8.12 @@ -260,9 +260,9 @@
    8.13  
    8.14    in
    8.15      thy2
    8.16 -    |> Theory.add_path (space_implode "_" new_type_names)
    8.17 +    |> Sign.add_path (space_implode "_" new_type_names)
    8.18      |> PureThy.add_thmss [(("recs", rec_thms), [])]
    8.19 -    ||> Theory.parent_path
    8.20 +    ||> Sign.parent_path
    8.21      |-> (fn thms => pair (reccomb_names, Library.flat thms))
    8.22    end;
    8.23  
     9.1 --- a/src/HOL/Tools/datatype_aux.ML	Tue Sep 25 15:34:35 2007 +0200
     9.2 +++ b/src/HOL/Tools/datatype_aux.ML	Tue Sep 25 17:06:14 2007 +0200
     9.3 @@ -70,26 +70,26 @@
     9.4  val quiet_mode = ref false;
     9.5  fun message s = if !quiet_mode then () else writeln s;
     9.6  
     9.7 -fun add_path flat_names s = if flat_names then I else Theory.add_path s;
     9.8 -fun parent_path flat_names = if flat_names then I else Theory.parent_path;
     9.9 +fun add_path flat_names s = if flat_names then I else Sign.add_path s;
    9.10 +fun parent_path flat_names = if flat_names then I else Sign.parent_path;
    9.11  
    9.12  
    9.13  (* store theorems in theory *)
    9.14  
    9.15  fun store_thmss_atts label tnames attss thmss =
    9.16    fold_map (fn ((tname, atts), thms) =>
    9.17 -    Theory.add_path tname
    9.18 +    Sign.add_path tname
    9.19      #> PureThy.add_thmss [((label, thms), atts)]
    9.20 -    #-> (fn thm::_ => Theory.parent_path #> pair thm)
    9.21 +    #-> (fn thm::_ => Sign.parent_path #> pair thm)
    9.22    ) (tnames ~~ attss ~~ thmss);
    9.23  
    9.24  fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
    9.25  
    9.26  fun store_thms_atts label tnames attss thmss =
    9.27    fold_map (fn ((tname, atts), thms) =>
    9.28 -    Theory.add_path tname
    9.29 +    Sign.add_path tname
    9.30      #> PureThy.add_thms [((label, thms), atts)]
    9.31 -    #-> (fn thm::_ => Theory.parent_path #> pair thm)
    9.32 +    #-> (fn thm::_ => Sign.parent_path #> pair thm)
    9.33    ) (tnames ~~ attss ~~ thmss);
    9.34  
    9.35  fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
    10.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Sep 25 15:34:35 2007 +0200
    10.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Sep 25 17:06:14 2007 +0200
    10.3 @@ -422,14 +422,14 @@
    10.4    (datatype_of_case (ProofContext.theory_of ctxt));
    10.5  
    10.6  fun add_case_tr' case_names thy =
    10.7 -  Theory.add_advanced_trfuns ([], [],
    10.8 +  Sign.add_advanced_trfuns ([], [],
    10.9      map (fn case_name =>
   10.10        let val case_name' = Sign.const_syntax_name thy case_name
   10.11        in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
   10.12        end) case_names, []) thy;
   10.13  
   10.14  val trfun_setup =
   10.15 -  Theory.add_advanced_trfuns ([],
   10.16 +  Sign.add_advanced_trfuns ([],
   10.17      [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
   10.18      [], []);
   10.19  
   10.20 @@ -490,9 +490,9 @@
   10.21  fun add_and_get_axioms_atts label tnames ts attss =
   10.22    fold_map (fn (tname, (atts, t)) => fn thy =>
   10.23      thy
   10.24 -    |> Theory.add_path tname
   10.25 +    |> Sign.add_path tname
   10.26      |> add_axiom label t atts
   10.27 -    ||> Theory.parent_path
   10.28 +    ||> Sign.parent_path
   10.29      |-> (fn [ax] => pair ax)) (tnames ~~ (attss ~~ ts));
   10.30  
   10.31  fun add_and_get_axioms label tnames ts =
   10.32 @@ -501,9 +501,9 @@
   10.33  fun add_and_get_axiomss label tnames tss =
   10.34    fold_map (fn (tname, ts) => fn thy =>
   10.35      thy
   10.36 -    |> Theory.add_path tname
   10.37 +    |> Sign.add_path tname
   10.38      |> add_axioms label ts []
   10.39 -    ||> Theory.parent_path
   10.40 +    ||> Sign.parent_path
   10.41      |-> (fn [ax] => pair ax)) (tnames ~~ tss);
   10.42  
   10.43  fun gen_specify_consts add args thy =
   10.44 @@ -594,10 +594,10 @@
   10.45  
   10.46      val ((([induct], [rec_thms]), inject), thy3) =
   10.47        thy2
   10.48 -      |> Theory.add_path (space_implode "_" new_type_names)
   10.49 +      |> Sign.add_path (space_implode "_" new_type_names)
   10.50        |> add_axiom "induct" (DatatypeProp.make_ind descr sorts) [case_names_induct]
   10.51        ||>> add_axioms "recs" rec_axs []
   10.52 -      ||> Theory.parent_path
   10.53 +      ||> Sign.parent_path
   10.54        ||>> add_and_get_axiomss "inject" new_type_names
   10.55              (DatatypeProp.make_injs descr sorts);
   10.56      val (distinct, thy4) = add_and_get_axiomss "distinct" new_type_names
   10.57 @@ -632,12 +632,12 @@
   10.58      val thy12 =
   10.59        thy11
   10.60        |> add_case_tr' case_names'
   10.61 -      |> Theory.add_path (space_implode "_" new_type_names)
   10.62 +      |> Sign.add_path (space_implode "_" new_type_names)
   10.63        |> add_rules simps case_thms rec_thms inject distinct
   10.64            weak_case_congs Simplifier.cong_add
   10.65        |> put_dt_infos dt_infos
   10.66        |> add_cases_induct dt_infos induct
   10.67 -      |> Theory.parent_path
   10.68 +      |> Sign.parent_path
   10.69        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   10.70        |> snd
   10.71        |> DatatypeInterpretation.data (map fst dt_infos);
   10.72 @@ -690,12 +690,12 @@
   10.73      val thy12 =
   10.74        thy10
   10.75        |> add_case_tr' case_names
   10.76 -      |> Theory.add_path (space_implode "_" new_type_names)
   10.77 +      |> Sign.add_path (space_implode "_" new_type_names)
   10.78        |> add_rules simps case_thms rec_thms inject distinct
   10.79            weak_case_congs (Simplifier.attrib (op addcongs))
   10.80        |> put_dt_infos dt_infos
   10.81        |> add_cases_induct dt_infos induct
   10.82 -      |> Theory.parent_path
   10.83 +      |> Sign.parent_path
   10.84        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
   10.85        |> DatatypeInterpretation.data (map fst dt_infos);
   10.86    in
   10.87 @@ -778,7 +778,7 @@
   10.88        thy8
   10.89        |> store_thmss "inject" new_type_names inject
   10.90        ||>> store_thmss "distinct" new_type_names distinct
   10.91 -      ||> Theory.add_path (space_implode "_" new_type_names)
   10.92 +      ||> Sign.add_path (space_implode "_" new_type_names)
   10.93        ||>> PureThy.add_thms [(("induct", induction), [case_names_induct])];
   10.94  
   10.95      val dt_infos = map (make_dt_info (length descr) descr sorts induction'
   10.96 @@ -795,7 +795,7 @@
   10.97             weak_case_congs (Simplifier.attrib (op addcongs))
   10.98        |> put_dt_infos dt_infos
   10.99        |> add_cases_induct dt_infos induction'
  10.100 -      |> Theory.parent_path
  10.101 +      |> Sign.parent_path
  10.102        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
  10.103        |> snd
  10.104        |> DatatypeInterpretation.data (map fst dt_infos);
  10.105 @@ -825,7 +825,7 @@
  10.106  
  10.107      val tmp_thy = thy |>
  10.108        Theory.copy |>
  10.109 -      Theory.add_types (map (fn (tvs, tname, mx, _) =>
  10.110 +      Sign.add_types (map (fn (tvs, tname, mx, _) =>
  10.111          (tname, length tvs, mx)) dts);
  10.112  
  10.113      val (tyvars, _, _, _)::_ = dts;
    11.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 15:34:35 2007 +0200
    11.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 17:06:14 2007 +0200
    11.3 @@ -130,10 +130,10 @@
    11.4      val ind_name = Thm.get_name induction;
    11.5      val vs = map (fn i => List.nth (pnames, i)) is;
    11.6      val (thm', thy') = thy
    11.7 -      |> Theory.absolute_path
    11.8 +      |> Sign.absolute_path
    11.9        |> PureThy.store_thm
   11.10          ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
   11.11 -      ||> Theory.restore_naming thy;
   11.12 +      ||> Sign.restore_naming thy;
   11.13  
   11.14      val ivs = rev (Term.add_vars (Logic.varify (DatatypeProp.make_ind [descr] sorts)) []);
   11.15      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
   11.16 @@ -197,9 +197,9 @@
   11.17  
   11.18      val exh_name = Thm.get_name exhaustion;
   11.19      val (thm', thy') = thy
   11.20 -      |> Theory.absolute_path
   11.21 +      |> Sign.absolute_path
   11.22        |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
   11.23 -      ||> Theory.restore_naming thy;
   11.24 +      ||> Sign.restore_naming thy;
   11.25  
   11.26      val P = Var (("P", 0), rT' --> HOLogic.boolT);
   11.27      val prf = forall_intr_prf (y, forall_intr_prf (P,
    12.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 25 15:34:35 2007 +0200
    12.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 25 17:06:14 2007 +0200
    12.3 @@ -236,7 +236,7 @@
    12.4            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
    12.5          val ([def_thm], thy') =
    12.6            thy
    12.7 -          |> Theory.add_consts_i [(cname', constrT, mx)]
    12.8 +          |> Sign.add_consts_i [(cname', constrT, mx)]
    12.9            |> (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)];
   12.10  
   12.11        in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
   12.12 @@ -259,7 +259,7 @@
   12.13        end;
   12.14  
   12.15      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
   12.16 -      ((thy3 |> Theory.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
   12.17 +      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
   12.18          hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
   12.19  
   12.20      (*********** isomorphisms for new types (introduced by typedef) ***********)
   12.21 @@ -616,9 +616,9 @@
   12.22  
   12.23      val ([dt_induct'], thy7) =
   12.24        thy6
   12.25 -      |> Theory.add_path big_name
   12.26 +      |> Sign.add_path big_name
   12.27        |> PureThy.add_thms [(("induct", dt_induct), [case_names_induct])]
   12.28 -      ||> Theory.parent_path;
   12.29 +      ||> Sign.parent_path;
   12.30  
   12.31    in
   12.32      ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
    13.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Sep 25 15:34:35 2007 +0200
    13.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Sep 25 17:06:14 2007 +0200
    13.3 @@ -292,14 +292,14 @@
    13.4      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
    13.5  
    13.6      val thy1 = thy |>
    13.7 -      Theory.root_path |>
    13.8 -      Theory.add_path (NameSpace.implode prfx);
    13.9 +      Sign.root_path |>
   13.10 +      Sign.add_path (NameSpace.implode prfx);
   13.11      val (ty_eqs, rlz_eqs) = split_list
   13.12        (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
   13.13  
   13.14      val thy1' = thy1 |>
   13.15        Theory.copy |>
   13.16 -      Theory.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
   13.17 +      Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
   13.18        fold (fn s => AxClass.axiomatize_arity_i
   13.19          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   13.20          Extraction.add_typeof_eqns_i ty_eqs;
   13.21 @@ -355,7 +355,7 @@
   13.22            ((Sign.base_name (name_of_thm intr), []),
   13.23             subst_atomic rlzpreds' (Logic.unvarify rintr)))
   13.24               (rintrs ~~ maps snd rss)) [] ||>
   13.25 -      Theory.absolute_path;
   13.26 +      Sign.absolute_path;
   13.27      val thy3 = PureThy.hide_thms false
   13.28        (map name_of_thm (#intrs ind_info)) thy3';
   13.29  
   13.30 @@ -480,7 +480,7 @@
   13.31          (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5,
   13.32             elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies)
   13.33  
   13.34 -  in Theory.restore_naming thy thy6 end;
   13.35 +  in Sign.restore_naming thy thy6 end;
   13.36  
   13.37  fun add_ind_realizers name rsets thy =
   13.38    let
    14.1 --- a/src/HOL/Tools/numeral_syntax.ML	Tue Sep 25 15:34:35 2007 +0200
    14.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Tue Sep 25 17:06:14 2007 +0200
    14.3 @@ -88,7 +88,7 @@
    14.4  (* theory setup *)
    14.5  
    14.6  val setup =
    14.7 -  Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
    14.8 -  Theory.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
    14.9 +  Sign.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
   14.10 +  Sign.add_trfunsT [(@{const_syntax Numeral.number_of}, numeral_tr')];
   14.11  
   14.12  end;
    15.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Sep 25 15:34:35 2007 +0200
    15.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Sep 25 17:06:14 2007 +0200
    15.3 @@ -285,7 +285,7 @@
    15.4        if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
    15.5      val (defs_thms', thy') =
    15.6        thy
    15.7 -      |> Theory.add_path primrec_name
    15.8 +      |> Sign.add_path primrec_name
    15.9        |> fold_map def (map (fn (name, t) => ((name, []), t)) defs');
   15.10      val rewrites = (map mk_meta_eq rec_rewrites) @ map snd defs_thms';
   15.11      val _ = message ("Proving equations for primrec function(s) " ^
   15.12 @@ -302,7 +302,7 @@
   15.13      |> snd
   15.14      |> note (("induct", []), [prepare_induct (#2 (hd dts)) rec_eqns])
   15.15      |> snd
   15.16 -    |> Theory.parent_path
   15.17 +    |> Sign.parent_path
   15.18      |> pair simps''
   15.19    end;
   15.20  
    16.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Sep 25 15:34:35 2007 +0200
    16.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Sep 25 17:06:14 2007 +0200
    16.3 @@ -215,7 +215,7 @@
    16.4  
    16.5      val ((simps' :: rules', [induct']), thy) =
    16.6        thy
    16.7 -      |> Theory.add_path bname
    16.8 +      |> Sign.add_path bname
    16.9        |> PureThy.add_thmss
   16.10          ((("simps", List.concat rules), simp_att) :: ((eq_names ~~ rules) ~~ eq_atts))
   16.11        ||>> PureThy.add_thms [(("induct", induct), [])];
   16.12 @@ -223,7 +223,7 @@
   16.13      val thy =
   16.14        thy
   16.15        |> put_recdef name result
   16.16 -      |> Theory.parent_path;
   16.17 +      |> Sign.parent_path;
   16.18    in (thy, result) end;
   16.19  
   16.20  val add_recdef = gen_add_recdef Tfl.define Attrib.attribute prepare_hints;
   16.21 @@ -245,9 +245,9 @@
   16.22      val (thy2, induct_rules) = tfl_fn thy1 congs name eqs;
   16.23      val ([induct_rules'], thy3) =
   16.24        thy2
   16.25 -      |> Theory.add_path bname
   16.26 +      |> Sign.add_path bname
   16.27        |> PureThy.add_thms [(("induct_rules", induct_rules), [])]
   16.28 -      ||> Theory.parent_path;
   16.29 +      ||> Sign.parent_path;
   16.30    in (thy3, {induct_rules = induct_rules'}) end;
   16.31  
   16.32  val defer_recdef = gen_defer_recdef Tfl.defer IsarCmd.apply_theorems;
    17.1 --- a/src/HOL/Tools/record_package.ML	Tue Sep 25 15:34:35 2007 +0200
    17.2 +++ b/src/HOL/Tools/record_package.ML	Tue Sep 25 17:06:14 2007 +0200
    17.3 @@ -1507,7 +1507,7 @@
    17.4      fun mk_defs () =
    17.5        thy
    17.6        |> extension_typedef name repT (alphas@[zeta])
    17.7 -      ||> Theory.add_consts_i
    17.8 +      ||> Sign.add_consts_i
    17.9              (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
   17.10        ||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
   17.11        ||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
   17.12 @@ -1780,7 +1780,7 @@
   17.13      (* 1st stage: extension_thy *)
   17.14      val (extension_thy,extT,ext_induct,ext_inject,ext_dest_convs,ext_split,u_convs) =
   17.15        thy
   17.16 -      |> Theory.add_path bname
   17.17 +      |> Sign.add_path bname
   17.18        |> extension_definition full extN fields names alphas_ext zeta moreT more vars;
   17.19  
   17.20      val _ = timing_msg "record preparing definitions";
   17.21 @@ -1900,16 +1900,16 @@
   17.22  
   17.23      fun mk_defs () =
   17.24        extension_thy
   17.25 -      |> Theory.add_trfuns
   17.26 +      |> Sign.add_trfuns
   17.27            ([],[],field_tr's, [])
   17.28 -      |> Theory.add_advanced_trfuns
   17.29 +      |> Sign.add_advanced_trfuns
   17.30            ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
   17.31 -      |> Theory.parent_path
   17.32 -      |> Theory.add_tyabbrs_i recordT_specs
   17.33 -      |> Theory.add_path bname
   17.34 -      |> Theory.add_consts_i
   17.35 +      |> Sign.parent_path
   17.36 +      |> Sign.add_tyabbrs_i recordT_specs
   17.37 +      |> Sign.add_path bname
   17.38 +      |> Sign.add_consts_i
   17.39            (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
   17.40 -      |> (Theory.add_consts_i o map Syntax.no_syn)
   17.41 +      |> (Sign.add_consts_i o map Syntax.no_syn)
   17.42            (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   17.43        |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
   17.44        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
   17.45 @@ -2169,7 +2169,7 @@
   17.46        |> add_record_splits extension_id (split_meta',split_object',split_ex',induct_scheme')
   17.47        |> add_extfields extension_name (fields @ [(full_moreN,moreT)])
   17.48        |> add_fieldext (extension_name,snd extension) (names @ [full_moreN])
   17.49 -      |> Theory.parent_path;
   17.50 +      |> Sign.parent_path;
   17.51  
   17.52    in final_thy
   17.53    end;
   17.54 @@ -2263,8 +2263,8 @@
   17.55  (* setup theory *)
   17.56  
   17.57  val setup =
   17.58 -  Theory.add_trfuns ([], parse_translation, [], []) #>
   17.59 -  Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
   17.60 +  Sign.add_trfuns ([], parse_translation, [], []) #>
   17.61 +  Sign.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
   17.62    (fn thy => (Simplifier.change_simpset_of thy
   17.63      (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy));
   17.64  
    18.1 --- a/src/HOL/Tools/string_syntax.ML	Tue Sep 25 15:34:35 2007 +0200
    18.2 +++ b/src/HOL/Tools/string_syntax.ML	Tue Sep 25 17:06:14 2007 +0200
    18.3 @@ -77,7 +77,7 @@
    18.4  (* theory setup *)
    18.5  
    18.6  val setup =
    18.7 -  Theory.add_trfuns
    18.8 +  Sign.add_trfuns
    18.9      ([("_Char", char_ast_tr), ("_String", string_ast_tr)], [], [],
   18.10        [("Char", char_ast_tr'), ("@list", list_ast_tr')]);
   18.11  
    19.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Sep 25 15:34:35 2007 +0200
    19.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Sep 25 17:06:14 2007 +0200
    19.3 @@ -54,8 +54,8 @@
    19.4  
    19.5  fun add_typedecls decls thy =
    19.6    if can (Theory.assert_super HOL.thy) thy then
    19.7 -    thy |> Theory.add_typedecls decls |> fold HOL_arity decls
    19.8 -  else thy |> Theory.add_typedecls decls;
    19.9 +    thy |> Sign.add_typedecls decls |> fold HOL_arity decls
   19.10 +  else thy |> Sign.add_typedecls decls;
   19.11  
   19.12  
   19.13  
   19.14 @@ -151,7 +151,7 @@
   19.15  
   19.16      fun typedef_result nonempty =
   19.17        add_typedecls [(t, vs, mx)]
   19.18 -      #> Theory.add_consts_i
   19.19 +      #> Sign.add_consts_i
   19.20         ((if def then [(name, setT', NoSyn)] else []) @
   19.21          [(Rep_name, newT --> oldT, NoSyn),
   19.22           (Abs_name, oldT --> newT, NoSyn)])
   19.23 @@ -168,7 +168,7 @@
   19.24            val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
   19.25                Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
   19.26              thy1
   19.27 -            |> Theory.add_path name
   19.28 +            |> Sign.add_path name
   19.29              |> PureThy.add_thms
   19.30                ([((Rep_name, make Rep), []),
   19.31                  ((Rep_name ^ "_inverse", make Rep_inverse), []),
   19.32 @@ -183,7 +183,7 @@
   19.33                    [RuleCases.case_names [Rep_name], InductAttrib.induct_set full_name]),
   19.34                  ((Abs_name ^ "_induct", make Abs_induct),
   19.35                    [RuleCases.case_names [Abs_name], InductAttrib.induct_type full_tname])])
   19.36 -            ||> Theory.parent_path;
   19.37 +            ||> Sign.parent_path;
   19.38            val info = {rep_type = oldT, abs_type = newT,
   19.39              Rep_name = full Rep_name, Abs_name = full Abs_name,
   19.40                type_definition = type_definition, set_def = set_def,
    20.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Sep 25 15:34:35 2007 +0200
    20.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Sep 25 17:06:14 2007 +0200
    20.3 @@ -156,14 +156,14 @@
    20.4  					::map one_con cons))));
    20.5      in foldr1 mk_conj (mapn one_comp 0 eqs)end ));
    20.6    fun add_one (thy,(dnam,axs,dfs)) = thy
    20.7 -	|> Theory.add_path dnam
    20.8 +	|> Sign.add_path dnam
    20.9  	|> add_defs_infer dfs
   20.10  	|> add_axioms_infer axs
   20.11 -	|> Theory.parent_path;
   20.12 +	|> Sign.parent_path;
   20.13    val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
   20.14 -in thy |> Theory.add_path comp_dnam  
   20.15 +in thy |> Sign.add_path comp_dnam  
   20.16         |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
   20.17 -       |> Theory.parent_path
   20.18 +       |> Sign.parent_path
   20.19  end;
   20.20  
   20.21  end; (* local *)
    21.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Tue Sep 25 15:34:35 2007 +0200
    21.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Tue Sep 25 17:06:14 2007 +0200
    21.3 @@ -105,7 +105,7 @@
    21.4      val cons''' = map snd eqs''';
    21.5      fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
    21.6      fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
    21.7 -    val thy'' = thy''' |> Theory.add_types     (map thy_type  dtnvs)
    21.8 +    val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
    21.9  		       |> fold (AxClass.axiomatize_arity_i o thy_arity) dtnvs;
   21.10      val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
   21.11      val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
   21.12 @@ -133,9 +133,9 @@
   21.13        |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
   21.14    in
   21.15      theorems_thy
   21.16 -    |> Theory.add_path (Sign.base_name comp_dnam)
   21.17 +    |> Sign.add_path (Sign.base_name comp_dnam)
   21.18      |> (snd o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
   21.19 -    |> Theory.parent_path
   21.20 +    |> Sign.parent_path
   21.21    end;
   21.22  
   21.23  val add_domain_i = gen_add_domain Sign.certify_typ;
    22.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Sep 25 15:34:35 2007 +0200
    22.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Sep 25 17:06:14 2007 +0200
    22.3 @@ -556,7 +556,7 @@
    22.4  
    22.5  in
    22.6    thy
    22.7 -    |> Theory.add_path (Sign.base_name dname)
    22.8 +    |> Sign.add_path (Sign.base_name dname)
    22.9      |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
   22.10          ("iso_rews" , iso_rews  ),
   22.11          ("exhaust"  , [exhaust] ),
   22.12 @@ -574,7 +574,7 @@
   22.13          ("copy_rews", copy_rews)])))
   22.14      |> (snd o PureThy.add_thmss
   22.15          [(("match_rews", mat_rews), [Simplifier.simp_add])])
   22.16 -    |> Theory.parent_path
   22.17 +    |> Sign.parent_path
   22.18      |> rpair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @
   22.19          pat_rews @ dist_les @ dist_eqs @ copy_rews)
   22.20  end; (* let *)
   22.21 @@ -941,7 +941,7 @@
   22.22      in pg [] goal tacs end;
   22.23  end; (* local *)
   22.24  
   22.25 -in thy |> Theory.add_path comp_dnam
   22.26 +in thy |> Sign.add_path comp_dnam
   22.27         |> (snd o (PureThy.add_thmss (map Thm.no_attributes [
   22.28  		("take_rews"  , take_rews  ),
   22.29  		("take_lemmas", take_lemmas),
   22.30 @@ -949,7 +949,7 @@
   22.31  		("finite_ind", [finite_ind]),
   22.32  		("ind"       , [ind       ]),
   22.33  		("coind"     , [coind     ])])))
   22.34 -       |> Theory.parent_path |> rpair take_rews
   22.35 +       |> Sign.parent_path |> rpair take_rews
   22.36  end; (* let *)
   22.37  end; (* local *)
   22.38  end; (* struct *)
    23.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Tue Sep 25 15:34:35 2007 +0200
    23.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Tue Sep 25 17:06:14 2007 +0200
    23.3 @@ -109,7 +109,7 @@
    23.4          theory
    23.5          |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
    23.6            (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
    23.7 -        |> Theory.add_path name
    23.8 +        |> Sign.add_path name
    23.9          |> PureThy.add_thms
   23.10              ([(("adm_" ^ name, admissible'), []),
   23.11                (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),
   23.12 @@ -118,7 +118,7 @@
   23.13                (("thelub_"  ^ name, typedef_thelub  OF cpo_thms), []),
   23.14                (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
   23.15          |> snd
   23.16 -        |> Theory.parent_path
   23.17 +        |> Sign.parent_path
   23.18        end;
   23.19  
   23.20      fun make_pcpo UUmem (type_def, less_def, set_def) theory =
   23.21 @@ -129,7 +129,7 @@
   23.22          theory
   23.23          |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
   23.24            (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
   23.25 -        |> Theory.add_path name
   23.26 +        |> Sign.add_path name
   23.27          |> PureThy.add_thms
   23.28              ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
   23.29                ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
   23.30 @@ -137,7 +137,7 @@
   23.31                ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
   23.32                ])
   23.33          |> snd
   23.34 -        |> Theory.parent_path
   23.35 +        |> Sign.parent_path
   23.36        end;
   23.37  
   23.38      fun pcpodef_result UUmem_admissible theory =
    24.1 --- a/src/Pure/Proof/extraction.ML	Tue Sep 25 15:34:35 2007 +0200
    24.2 +++ b/src/Pure/Proof/extraction.ML	Tue Sep 25 17:06:14 2007 +0200
    24.3 @@ -37,7 +37,7 @@
    24.4  fun add_syntax thy =
    24.5    thy
    24.6    |> Theory.copy
    24.7 -  |> Theory.root_path
    24.8 +  |> Sign.root_path
    24.9    |> Sign.add_types [("Type", 0, NoSyn), ("Null", 0, NoSyn)]
   24.10    |> Sign.add_consts
   24.11        [("typeof", "'b::{} => Type", NoSyn),
    25.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 25 15:34:35 2007 +0200
    25.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 25 17:06:14 2007 +0200
    25.3 @@ -92,7 +92,7 @@
    25.4  
    25.5  in
    25.6  
    25.7 -val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
    25.8 +val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
    25.9  
   25.10  end;
   25.11  
    26.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 25 15:34:35 2007 +0200
    26.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 25 17:06:14 2007 +0200
    26.3 @@ -105,7 +105,7 @@
    26.4  
    26.5  in
    26.6  
    26.7 -val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
    26.8 +val _ = Context.add_setup (Sign.add_tokentrfuns proof_general_trans);
    26.9  
   26.10  end;
   26.11  
    27.1 --- a/src/Pure/axclass.ML	Tue Sep 25 15:34:35 2007 +0200
    27.2 +++ b/src/Pure/axclass.ML	Tue Sep 25 17:06:14 2007 +0200
    27.3 @@ -382,9 +382,9 @@
    27.4          (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
    27.5    in
    27.6      thy
    27.7 -    |> Theory.add_path prefix
    27.8 +    |> Sign.add_path prefix
    27.9      |> fold_map add_const consts
   27.10 -    ||> Theory.restore_naming thy
   27.11 +    ||> Sign.restore_naming thy
   27.12      |-> (fn cs => mk_axioms cs
   27.13      #-> (fn axioms_prop => define_class (name, superclasses)
   27.14             (map fst cs @ other_consts) axioms_prop
    28.1 --- a/src/ZF/Tools/datatype_package.ML	Tue Sep 25 15:34:35 2007 +0200
    28.2 +++ b/src/ZF/Tools/datatype_package.ML	Tue Sep 25 17:06:14 2007 +0200
    28.3 @@ -61,7 +61,7 @@
    28.4    val rec_base_names = map Sign.base_name rec_names
    28.5    val big_rec_base_name = space_implode "_" rec_base_names
    28.6  
    28.7 -  val thy_path = thy |> Theory.add_path big_rec_base_name
    28.8 +  val thy_path = thy |> Sign.add_path big_rec_base_name
    28.9  
   28.10    val big_rec_name = Sign.intern_const thy_path big_rec_base_name;
   28.11  
   28.12 @@ -229,13 +229,13 @@
   28.13  
   28.14    fun add_recursor thy =
   28.15        if need_recursor then
   28.16 -           thy |> Theory.add_consts_i
   28.17 +           thy |> Sign.add_consts_i
   28.18                      [(recursor_base_name, recursor_typ, NoSyn)]
   28.19                 |> (snd o PureThy.add_defs_i false [Thm.no_attributes recursor_def])
   28.20        else thy;
   28.21  
   28.22    val (con_defs, thy0) = thy_path
   28.23 -             |> Theory.add_consts_i
   28.24 +             |> Sign.add_consts_i
   28.25                   ((case_base_name, case_typ, NoSyn) ::
   28.26                    map #1 (List.concat con_ty_lists))
   28.27               |> PureThy.add_defs_i false
   28.28 @@ -244,7 +244,7 @@
   28.29                     List.concat (ListPair.map mk_con_defs
   28.30                           (1 upto npart, con_ty_lists))))
   28.31               ||> add_recursor
   28.32 -             ||> Theory.parent_path
   28.33 +             ||> Sign.parent_path
   28.34  
   28.35    val intr_names = map #2 (List.concat con_ty_lists);
   28.36    val (thy1, ind_result) =
   28.37 @@ -365,7 +365,7 @@
   28.38  
   28.39   in
   28.40    (*Updating theory components: simprules and datatype info*)
   28.41 -  (thy1 |> Theory.add_path big_rec_base_name
   28.42 +  (thy1 |> Sign.add_path big_rec_base_name
   28.43          |> PureThy.add_thmss
   28.44           [(("simps", simps), [Simplifier.simp_add]),
   28.45            (("", intrs), [Classical.safe_intro NONE]),
   28.46 @@ -376,7 +376,7 @@
   28.47            (("free_elims", free_SEs), [])] |> snd
   28.48          |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
   28.49          |> ConstructorsData.map (fold Symtab.update con_pairs)
   28.50 -        |> Theory.parent_path,
   28.51 +        |> Sign.parent_path,
   28.52     ind_result,
   28.53     {con_defs = con_defs,
   28.54      case_eqns = case_eqns,
    29.1 --- a/src/ZF/Tools/induct_tacs.ML	Tue Sep 25 15:34:35 2007 +0200
    29.2 +++ b/src/ZF/Tools/induct_tacs.ML	Tue Sep 25 17:06:14 2007 +0200
    29.3 @@ -157,11 +157,11 @@
    29.4  
    29.5    in
    29.6      thy
    29.7 -    |> Theory.add_path (Sign.base_name big_rec_name)
    29.8 +    |> Sign.add_path (Sign.base_name big_rec_name)
    29.9      |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add])] |> snd
   29.10      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   29.11      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
   29.12 -    |> Theory.parent_path
   29.13 +    |> Sign.parent_path
   29.14    end;
   29.15  
   29.16  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =
    30.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Sep 25 15:34:35 2007 +0200
    30.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Sep 25 17:06:14 2007 +0200
    30.3 @@ -172,7 +172,7 @@
    30.4    (*add definitions of the inductive sets*)
    30.5    val (_, thy1) =
    30.6      thy
    30.7 -    |> Theory.add_path big_rec_base_name
    30.8 +    |> Sign.add_path big_rec_base_name
    30.9      |> PureThy.add_defs_i false (map Thm.no_attributes axpairs)
   30.10  
   30.11  
   30.12 @@ -535,7 +535,7 @@
   30.13    val (intrs'', thy4) =
   30.14      thy3
   30.15      |> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs)
   30.16 -    ||> Theory.parent_path;
   30.17 +    ||> Sign.parent_path;
   30.18    in
   30.19      (thy4,
   30.20        {defs = defs',
    31.1 --- a/src/ZF/Tools/numeral_syntax.ML	Tue Sep 25 15:34:35 2007 +0200
    31.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Tue Sep 25 17:06:14 2007 +0200
    31.3 @@ -100,7 +100,7 @@
    31.4  
    31.5  
    31.6  val setup =
    31.7 - (Theory.add_trfuns ([], [("_Int", int_tr)], [], []) #>
    31.8 -  Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
    31.9 + (Sign.add_trfuns ([], [("_Int", int_tr)], [], []) #>
   31.10 +  Sign.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
   31.11  
   31.12  end;
    32.1 --- a/src/ZF/Tools/primrec_package.ML	Tue Sep 25 15:34:35 2007 +0200
    32.2 +++ b/src/ZF/Tools/primrec_package.ML	Tue Sep 25 17:06:14 2007 +0200
    32.3 @@ -176,7 +176,7 @@
    32.4      val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
    32.5  
    32.6      val ([def_thm], thy1) = thy
    32.7 -      |> Theory.add_path (Sign.base_name fname)
    32.8 +      |> Sign.add_path (Sign.base_name fname)
    32.9        |> (PureThy.add_defs_i false o map Thm.no_attributes) [def];
   32.10  
   32.11      val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
   32.12 @@ -192,7 +192,7 @@
   32.13      val (_, thy3) =
   32.14        thy2
   32.15        |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]
   32.16 -      ||> Theory.parent_path;
   32.17 +      ||> Sign.parent_path;
   32.18    in (thy3, eqn_thms') end;
   32.19  
   32.20  fun add_primrec args thy =