Theory.sign_of;
authorwenzelm
Wed Mar 17 16:53:46 1999 +0100 (1999-03-17)
changeset 63943d9fd50fcc43
parent 6393 b8dafa978382
child 6395 5abd0d044adf
Theory.sign_of;
src/HOL/Arith.ML
src/HOL/Integ/Bin.ML
src/HOL/List.ML
src/HOL/Prod.ML
src/HOL/Set.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/record_package.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Mar 17 16:53:32 1999 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Mar 17 16:53:46 1999 +0100
     1.3 @@ -763,7 +763,7 @@
     1.4    val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
     1.5  end;
     1.6  
     1.7 -fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n);
     1.8 +fun mk_cnat n = cterm_of (Theory.sign_of Nat.thy) (HOLogic.mk_nat n);
     1.9  
    1.10  fun gen_multiply_tac rule k =
    1.11    if k > 0 then
    1.12 @@ -807,7 +807,7 @@
    1.13  
    1.14  (** prepare nat_cancel simprocs **)
    1.15  
    1.16 -fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar);
    1.17 +fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termTVar);
    1.18  val prep_pats = map prep_pat;
    1.19  
    1.20  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
    1.21 @@ -954,7 +954,7 @@
    1.22  val fast_arith_tac = Fast_Arith.lin_arith_tac;
    1.23  
    1.24  val nat_arith_simproc_pats =
    1.25 -  map (fn s => Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.boolT))
    1.26 +  map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT))
    1.27        ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
    1.28  
    1.29  val fast_nat_arith_simproc = mk_simproc "fast_nat_arith" nat_arith_simproc_pats
     2.1 --- a/src/HOL/Integ/Bin.ML	Wed Mar 17 16:53:32 1999 +0100
     2.2 +++ b/src/HOL/Integ/Bin.ML	Wed Mar 17 16:53:46 1999 +0100
     2.3 @@ -482,7 +482,7 @@
     2.4  
     2.5  
     2.6  val int_arith_simproc_pats =
     2.7 -  map (fn s => Thm.read_cterm (sign_of Int.thy) (s, HOLogic.boolT))
     2.8 +  map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
     2.9        ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
    2.10  
    2.11  val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
     3.1 --- a/src/HOL/List.ML	Wed Mar 17 16:53:32 1999 +0100
     3.2 +++ b/src/HOL/List.ML	Wed Mar 17 16:53:46 1999 +0100
     3.3 @@ -251,7 +251,7 @@
     3.4  local
     3.5  
     3.6  val list_eq_pattern =
     3.7 -  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
     3.8 +  Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
     3.9  
    3.10  fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
    3.11        (case xs of Const("List.list.[]",_) => cons | _ => last xs)
     4.1 --- a/src/HOL/Prod.ML	Wed Mar 17 16:53:32 1999 +0100
     4.2 +++ b/src/HOL/Prod.ML	Wed Mar 17 16:53:46 1999 +0100
     4.3 @@ -136,7 +136,7 @@
     4.4    using split_eta a rewrite rule is not general enough, and using 
     4.5    cond_split_eta directly would render some existing proofs very inefficient*)
     4.6  local
     4.7 -  val split_eta_pat = Thm.read_cterm (sign_of thy) 
     4.8 +  val split_eta_pat = Thm.read_cterm (Theory.sign_of thy) 
     4.9  		("split (%x. split (%y. f x y))", HOLogic.termTVar);
    4.10    val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta);
    4.11    fun  Pair_pat 0      (Bound 0) = true
    4.12 @@ -431,7 +431,7 @@
    4.13  (*simplification procedure for unit_eq.
    4.14    Cannot use this rule directly -- it loops!*)
    4.15  local
    4.16 -  val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT));
    4.17 +  val unit_pat = Thm.cterm_of (Theory.sign_of thy) (Free ("x", HOLogic.unitT));
    4.18    val unit_meta_eq = standard (mk_meta_eq unit_eq);
    4.19    fun proc _ _ t =
    4.20      if HOLogic.is_unit t then None
     5.1 --- a/src/HOL/Set.ML	Wed Mar 17 16:53:32 1999 +0100
     5.2 +++ b/src/HOL/Set.ML	Wed Mar 17 16:53:46 1999 +0100
     5.3 @@ -656,9 +656,9 @@
     5.4  (*Split ifs on either side of the membership relation.
     5.5  	Not for Addsimps -- can cause goals to blow up!*)
     5.6  bind_thm ("split_if_mem1", 
     5.7 -    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
     5.8 +    read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
     5.9  bind_thm ("split_if_mem2", 
    5.10 -    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
    5.11 +    read_instantiate_sg (Theory.sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
    5.12  
    5.13  val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
    5.14  		  split_if_mem1, split_if_mem2];
     6.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Mar 17 16:53:32 1999 +0100
     6.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Mar 17 16:53:46 1999 +0100
     6.3 @@ -52,7 +52,7 @@
     6.4  
     6.5  open DatatypeAux;
     6.6  
     6.7 -val thin = read_instantiate_sg (sign_of Set.thy) [("V", "?X : ?Y")] thin_rl;
     6.8 +val thin = read_instantiate_sg (Theory.sign_of Set.thy) [("V", "?X : ?Y")] thin_rl;
     6.9  
    6.10  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    6.11  
    6.12 @@ -75,7 +75,7 @@
    6.13          val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", 0), T), Bound 0) $
    6.14            Var (("P", 0), HOLogic.boolT))
    6.15          val insts = take (i, dummyPs) @ (P::(drop (i + 1, dummyPs)));
    6.16 -        val cert = cterm_of (sign_of thy);
    6.17 +        val cert = cterm_of (Theory.sign_of thy);
    6.18          val insts' = (map cert induct_Ps) ~~ (map cert insts);
    6.19          val induct' = refl RS ((nth_elem (i,
    6.20            split_conj_thm (cterm_instantiate insts' induct))) RSN (2, rev_mp))
    6.21 @@ -112,7 +112,7 @@
    6.22      val induct_Ps = map head_of (dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    6.23  
    6.24      val big_rec_name' = big_name ^ "_rec_set";
    6.25 -    val rec_set_names = map (Sign.full_name (sign_of thy0))
    6.26 +    val rec_set_names = map (Sign.full_name (Theory.sign_of thy0))
    6.27        (if length descr' = 1 then [big_rec_name'] else
    6.28          (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
    6.29            (1 upto (length descr'))));
    6.30 @@ -221,7 +221,7 @@
    6.31              absfree ("y", T2, HOLogic.mk_mem (HOLogic.mk_prod
    6.32                (mk_Free "x" T1 i, Free ("y", T2)), set_t)))
    6.33                  (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
    6.34 -        val cert = cterm_of (sign_of thy1)
    6.35 +        val cert = cterm_of (Theory.sign_of thy1)
    6.36          val insts = map (fn ((i, T), t) => absfree ("x" ^ (string_of_int i), T, t))
    6.37            ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
    6.38          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
    6.39 @@ -239,7 +239,7 @@
    6.40      (* define primrec combinators *)
    6.41  
    6.42      val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
    6.43 -    val reccomb_names = map (Sign.full_name (sign_of thy1))
    6.44 +    val reccomb_names = map (Sign.full_name (Theory.sign_of thy1))
    6.45        (if length descr' = 1 then [big_reccomb_name] else
    6.46          (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
    6.47            (1 upto (length descr'))));
    6.48 @@ -266,7 +266,7 @@
    6.49      val _ = message "Proving characteristic theorems for primrec combinators..."
    6.50  
    6.51      val rec_thms = map (fn t => prove_goalw_cterm reccomb_defs
    6.52 -      (cterm_of (sign_of thy2) t) (fn _ =>
    6.53 +      (cterm_of (Theory.sign_of thy2) t) (fn _ =>
    6.54          [rtac select1_equality 1,
    6.55           resolve_tac rec_unique_thms 1,
    6.56           resolve_tac rec_intrs 1,
    6.57 @@ -302,7 +302,7 @@
    6.58        end) constrs) descr';
    6.59  
    6.60      val case_names = map (fn s =>
    6.61 -      Sign.full_name (sign_of thy1) (s ^ "_case")) new_type_names;
    6.62 +      Sign.full_name (Theory.sign_of thy1) (s ^ "_case")) new_type_names;
    6.63  
    6.64      (* define case combinators via primrec combinators *)
    6.65  
    6.66 @@ -338,7 +338,7 @@
    6.67            (take (length newTs, reccomb_names)));
    6.68  
    6.69      val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
    6.70 -      (map mk_meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
    6.71 +      (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t)
    6.72          (fn _ => [rtac refl 1])))
    6.73            (DatatypeProp.make_cases new_type_names descr sorts thy2);
    6.74  
    6.75 @@ -374,8 +374,8 @@
    6.76            val mk_abs = foldr (fn (T, t') => Abs ("x", T, t'));
    6.77            val fs = map mk_abs (Tss ~~ ts);
    6.78            val fTs = map (fn Ts => Ts ---> HOLogic.natT) Tss;
    6.79 -          val ord_name = Sign.full_name (sign_of thy) (tname ^ "_ord");
    6.80 -          val case_name = Sign.intern_const (sign_of thy) (tname ^ "_case");
    6.81 +          val ord_name = Sign.full_name (Theory.sign_of thy) (tname ^ "_ord");
    6.82 +          val case_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_case");
    6.83            val ordT = T --> HOLogic.natT;
    6.84            val caseT = fTs ---> ordT;
    6.85            val defpair = (tname ^ "_ord_def", Logic.mk_equals
    6.86 @@ -395,7 +395,7 @@
    6.87      fun prove_distinct_thms _ [] = []
    6.88        | prove_distinct_thms dist_rewrites' (t::_::ts) =
    6.89            let
    6.90 -            val dist_thm = prove_goalw_cterm [] (cterm_of (sign_of thy2) t) (fn _ =>
    6.91 +            val dist_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy2) t) (fn _ =>
    6.92                [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    6.93            in dist_thm::(standard (dist_thm RS not_sym))::
    6.94              (prove_distinct_thms dist_rewrites' ts)
    6.95 @@ -409,7 +409,7 @@
    6.96            let
    6.97              val t::ts' = rev ts;
    6.98              val (_ $ (_ $ (_ $ (f $ _) $ _))) = hd (Logic.strip_imp_prems t);
    6.99 -            val cert = cterm_of (sign_of thy2);
   6.100 +            val cert = cterm_of (Theory.sign_of thy2);
   6.101              val distinct_lemma' = cterm_instantiate
   6.102                [(cert distinct_f, cert f)] distinct_lemma;
   6.103              val rewrites = ord_defs @ (map mk_meta_eq case_thms)
   6.104 @@ -439,7 +439,7 @@
   6.105      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'),
   6.106          exhaustion), case_thms'), T) =
   6.107        let
   6.108 -        val cert = cterm_of (sign_of thy);
   6.109 +        val cert = cterm_of (Theory.sign_of thy);
   6.110          val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
   6.111          val exhaustion' = cterm_instantiate
   6.112            [(cert lhs, cert (Free ("x", T)))] exhaustion;
   6.113 @@ -475,9 +475,9 @@
   6.114      val recTs = get_rec_types descr' sorts;
   6.115  
   6.116      val big_size_name = space_implode "_" new_type_names ^ "_size";
   6.117 -    val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy1))) "size";
   6.118 +    val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy1))) "size";
   6.119      val size_names = replicate (length (hd descr)) size_name @
   6.120 -      map (Sign.full_name (sign_of thy1))
   6.121 +      map (Sign.full_name (Theory.sign_of thy1))
   6.122          (if length (flat (tl descr)) = 1 then [big_size_name] else
   6.123            map (fn i => big_size_name ^ "_" ^ string_of_int i)
   6.124              (1 upto length (flat (tl descr))));
   6.125 @@ -513,7 +513,7 @@
   6.126      val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
   6.127  
   6.128      val size_thms = map (fn t => prove_goalw_cterm rewrites
   6.129 -      (cterm_of (sign_of thy') t) (fn _ => [rtac refl 1]))
   6.130 +      (cterm_of (Theory.sign_of thy') t) (fn _ => [rtac refl 1]))
   6.131          (DatatypeProp.make_size new_type_names descr sorts thy')
   6.132  
   6.133    in
   6.134 @@ -536,7 +536,7 @@
   6.135                hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
   6.136            | tac i n = rtac disjI2 i THEN tac i (n - 1)
   6.137        in 
   6.138 -        prove_goalw_cterm [] (cterm_of (sign_of thy) t) (fn _ =>
   6.139 +        prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) t) (fn _ =>
   6.140            [rtac allI 1,
   6.141             exh_tac (K exhaustion) 1,
   6.142             ALLGOALS (fn i => tac i (i-1))])
   6.143 @@ -555,7 +555,7 @@
   6.144        let
   6.145          val (Const ("==>", _) $ tm $ _) = t;
   6.146          val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
   6.147 -        val cert = cterm_of (sign_of thy);
   6.148 +        val cert = cterm_of (Theory.sign_of thy);
   6.149          val nchotomy' = nchotomy RS spec;
   6.150          val nchotomy'' = cterm_instantiate
   6.151            [(cert (hd (add_term_vars (concl_of nchotomy', []))), cert Ma)] nchotomy'
     7.1 --- a/src/HOL/Tools/datatype_aux.ML	Wed Mar 17 16:53:32 1999 +0100
     7.2 +++ b/src/HOL/Tools/datatype_aux.ML	Wed Mar 17 16:53:46 1999 +0100
     7.3 @@ -68,7 +68,7 @@
     7.4  fun foldl1 f (x::xs) = foldl f (x, xs);
     7.5  
     7.6  fun get_thy name thy = find_first
     7.7 -  (equal name o Sign.name_of o sign_of) (ancestors_of thy);
     7.8 +  (equal name o Sign.name_of o Theory.sign_of) (Theory.ancestors_of thy);
     7.9  
    7.10  fun add_path flat_names s = if flat_names then I else Theory.add_path s;
    7.11  fun parent_path flat_names = if flat_names then I else Theory.parent_path;
    7.12 @@ -113,7 +113,7 @@
    7.13          None => let val [Free (s, T)] = add_term_frees (t2, [])
    7.14            in absfree (s, T, t2) end
    7.15        | Some (_ $ t' $ _) => Abs ("x", fastype_of t', abstract_over (t', t2)))
    7.16 -    val cert = cterm_of (sign_of_thm st);
    7.17 +    val cert = cterm_of (Thm.sign_of_thm st);
    7.18      val Ps = map (cert o head_of o snd o getP) ts;
    7.19      val indrule' = cterm_instantiate (Ps ~~
    7.20        (map (cert o abstr o getP) ts')) indrule
    7.21 @@ -125,7 +125,7 @@
    7.22  
    7.23  fun exh_tac exh_thm_of i state =
    7.24    let
    7.25 -    val sg = sign_of_thm state;
    7.26 +    val sg = Thm.sign_of_thm state;
    7.27      val prem = nth_elem (i - 1, prems_of state);
    7.28      val params = Logic.strip_params prem;
    7.29      val (_, Type (tname, _)) = hd (rev params);
     8.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Mar 17 16:53:32 1999 +0100
     8.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 17 16:53:46 1999 +0100
     8.3 @@ -111,7 +111,7 @@
     8.4      Some info => info
     8.5    | None => error ("Unknown datatype " ^ quote name));
     8.6  
     8.7 -val datatype_info = datatype_info_sg o sign_of;
     8.8 +val datatype_info = datatype_info_sg o Theory.sign_of;
     8.9  
    8.10  fun constrs_of thy tname =
    8.11    let
    8.12 @@ -119,14 +119,14 @@
    8.13      val (_, _, constrs) = the (assoc (descr, index))
    8.14    in
    8.15      Some (map (fn (cname, _) =>
    8.16 -      Const (cname, the (Sign.const_type (sign_of thy) cname))) constrs)
    8.17 +      Const (cname, the (Sign.const_type (Theory.sign_of thy) cname))) constrs)
    8.18    end handle _ => None;
    8.19  
    8.20  fun case_const_of thy tname =
    8.21    let
    8.22      val {case_name, ...} = datatype_info thy tname;
    8.23    in
    8.24 -    Some (Const (case_name, the (Sign.const_type (sign_of thy) case_name)))
    8.25 +    Some (Const (case_name, the (Sign.const_type (Theory.sign_of thy) case_name)))
    8.26    end handle _ => None;
    8.27  
    8.28  fun find_tname var Bi =
    8.29 @@ -340,8 +340,8 @@
    8.30            (case_names ~~ newTs ~~ case_fn_Ts)) |>
    8.31        Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr);
    8.32  
    8.33 -    val reccomb_names' = map (Sign.intern_const (sign_of thy2')) reccomb_names;
    8.34 -    val case_names' = map (Sign.intern_const (sign_of thy2')) case_names;
    8.35 +    val reccomb_names' = map (Sign.intern_const (Theory.sign_of thy2')) reccomb_names;
    8.36 +    val case_names' = map (Sign.intern_const (Theory.sign_of thy2')) case_names;
    8.37  
    8.38      val thy2 = thy2' |>
    8.39  
    8.40 @@ -501,7 +501,7 @@
    8.41        |> app_thmss raw_distinct
    8.42        |> apfst (app_thmss raw_inject)
    8.43        |> apfst (apfst (app_thm raw_induction));
    8.44 -    val sign = sign_of thy1;
    8.45 +    val sign = Theory.sign_of thy1;
    8.46  
    8.47      val induction' = freezeT induction;
    8.48  
    8.49 @@ -549,7 +549,7 @@
    8.50      val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
    8.51        [descr] sorts nchotomys case_thms thy6;
    8.52      val (thy8, size_thms) =
    8.53 -      if exists (equal "Arith") (Sign.stamp_names_of (sign_of thy7)) then
    8.54 +      if exists (equal "Arith") (Sign.stamp_names_of (Theory.sign_of thy7)) then
    8.55          DatatypeAbsProofs.prove_size_thms false new_type_names
    8.56            [descr] sorts reccomb_names rec_thms thy7
    8.57        else (thy7, []);
    8.58 @@ -600,7 +600,7 @@
    8.59        Theory.add_types (map (fn (tvs, tname, mx, _) =>
    8.60          (tname, length tvs, mx)) dts);
    8.61  
    8.62 -    val sign = sign_of tmp_thy;
    8.63 +    val sign = Theory.sign_of tmp_thy;
    8.64  
    8.65      val (tyvars, _, _, _)::_ = dts;
    8.66      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
     9.1 --- a/src/HOL/Tools/datatype_prop.ML	Wed Mar 17 16:53:32 1999 +0100
     9.2 +++ b/src/HOL/Tools/datatype_prop.ML	Wed Mar 17 16:53:46 1999 +0100
     9.3 @@ -162,7 +162,7 @@
     9.4  
     9.5  fun make_primrecs new_type_names descr sorts thy =
     9.6    let
     9.7 -    val sign = sign_of thy;
     9.8 +    val sign = Theory.sign_of thy;
     9.9  
    9.10      val descr' = flat descr;
    9.11      val recTs = get_rec_types descr' sorts;
    9.12 @@ -229,7 +229,7 @@
    9.13          in Ts ---> T' end) constrs) (hd descr);
    9.14  
    9.15      val case_names = map (fn s =>
    9.16 -      Sign.intern_const (sign_of thy) (s ^ "_case")) new_type_names
    9.17 +      Sign.intern_const (Theory.sign_of thy) (s ^ "_case")) new_type_names
    9.18    in
    9.19      map (fn ((name, Ts), T) => list_comb
    9.20        (Const (name, Ts @ [T] ---> T'),
    9.21 @@ -296,7 +296,7 @@
    9.22  
    9.23      fun make_distincts_2 T tname i constrs =
    9.24        let
    9.25 -        val ord_name = Sign.intern_const (sign_of thy) (tname ^ "_ord");
    9.26 +        val ord_name = Sign.intern_const (Theory.sign_of thy) (tname ^ "_ord");
    9.27          val ord_t = Const (ord_name, T --> HOLogic.natT)
    9.28  
    9.29        in (case constrs of
    9.30 @@ -403,9 +403,9 @@
    9.31      val recTs = get_rec_types descr' sorts;
    9.32  
    9.33      val big_size_name = space_implode "_" new_type_names ^ "_size";
    9.34 -    val size_name = Sign.intern_const (sign_of (the (get_thy "Arith" thy))) "size";
    9.35 +    val size_name = Sign.intern_const (Theory.sign_of (the (get_thy "Arith" thy))) "size";
    9.36      val size_names = replicate (length (hd descr)) size_name @
    9.37 -      map (Sign.intern_const (sign_of thy))
    9.38 +      map (Sign.intern_const (Theory.sign_of thy))
    9.39          (if length (flat (tl descr)) = 1 then [big_size_name] else
    9.40            map (fn i => big_size_name ^ "_" ^ string_of_int i)
    9.41              (1 upto length (flat (tl descr))));
    10.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 17 16:53:32 1999 +0100
    10.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 17 16:53:46 1999 +0100
    10.3 @@ -30,10 +30,10 @@
    10.4  
    10.5  (* figure out internal names *)
    10.6  
    10.7 -val image_name = Sign.intern_const (sign_of Set.thy) "op ``";
    10.8 -val UNIV_name = Sign.intern_const (sign_of Set.thy) "UNIV";
    10.9 -val inj_on_name = Sign.intern_const (sign_of Fun.thy) "inj_on";
   10.10 -val inv_name = Sign.intern_const (sign_of Fun.thy) "inv";
   10.11 +val image_name = Sign.intern_const (Theory.sign_of Set.thy) "op ``";
   10.12 +val UNIV_name = Sign.intern_const (Theory.sign_of Set.thy) "UNIV";
   10.13 +val inj_on_name = Sign.intern_const (Theory.sign_of Fun.thy) "inj_on";
   10.14 +val inv_name = Sign.intern_const (Theory.sign_of Fun.thy) "inv";
   10.15  
   10.16  fun exh_thm_of (dt_info : datatype_info Symtab.table) tname =
   10.17    #exhaustion (the (Symtab.lookup (dt_info, tname)));
   10.18 @@ -44,9 +44,9 @@
   10.19        new_type_names descr sorts types_syntax constr_syntax thy =
   10.20    let
   10.21      val Univ_thy = the (get_thy "Univ" thy);
   10.22 -    val node_name = Sign.intern_tycon (sign_of Univ_thy) "node";
   10.23 +    val node_name = Sign.intern_tycon (Theory.sign_of Univ_thy) "node";
   10.24      val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name] =
   10.25 -      map (Sign.intern_const (sign_of Univ_thy))
   10.26 +      map (Sign.intern_const (Theory.sign_of Univ_thy))
   10.27          ["In0", "In1", "Scons", "Leaf", "Numb"];
   10.28      val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
   10.29        In0_not_In1, In1_not_In0] = map (get_thm Univ_thy)
   10.30 @@ -58,7 +58,7 @@
   10.31      val big_name = space_implode "_" new_type_names;
   10.32      val thy1 = add_path flat_names big_name thy;
   10.33      val big_rec_name = big_name ^ "_rep_set";
   10.34 -    val rep_set_names = map (Sign.full_name (sign_of thy1))
   10.35 +    val rep_set_names = map (Sign.full_name (Theory.sign_of thy1))
   10.36        (if length descr' = 1 then [big_rec_name] else
   10.37          (map ((curry (op ^) (big_rec_name ^ "_")) o string_of_int)
   10.38            (1 upto (length descr'))));
   10.39 @@ -153,8 +153,8 @@
   10.40      val rep_names = map (curry op ^ "Rep_") new_type_names;
   10.41      val rep_names' = map (fn i => big_rep_name ^ (string_of_int i))
   10.42        (1 upto (length (flat (tl descr))));
   10.43 -    val all_rep_names = map (Sign.intern_const (sign_of thy3)) rep_names @
   10.44 -      map (Sign.full_name (sign_of thy3)) rep_names';
   10.45 +    val all_rep_names = map (Sign.intern_const (Theory.sign_of thy3)) rep_names @
   10.46 +      map (Sign.full_name (Theory.sign_of thy3)) rep_names';
   10.47  
   10.48      (* isomorphism declarations *)
   10.49  
   10.50 @@ -176,8 +176,8 @@
   10.51  
   10.52          val (_, l_args, r_args) = foldr constr_arg (cargs, (1, [], []));
   10.53          val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T;
   10.54 -        val abs_name = Sign.intern_const (sign_of thy) ("Abs_" ^ tname);
   10.55 -        val rep_name = Sign.intern_const (sign_of thy) ("Rep_" ^ tname);
   10.56 +        val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname);
   10.57 +        val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname);
   10.58          val lhs = list_comb (Const (cname, constrT), l_args);
   10.59          val rhs = mk_univ_inj r_args n i;
   10.60          val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
   10.61 @@ -197,7 +197,7 @@
   10.62          ((((_, (_, _, constrs)), tname), T), constr_syntax)) =
   10.63        let
   10.64          val _ $ (_ $ (cong_f $ _) $ _) = concl_of arg_cong;
   10.65 -        val sg = sign_of thy;
   10.66 +        val sg = Theory.sign_of thy;
   10.67          val rep_const = cterm_of sg
   10.68            (Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT));
   10.69          val cong' = cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong;
   10.70 @@ -231,7 +231,7 @@
   10.71  
   10.72      fun prove_newT_iso_inj_thm (((s, (thm1, thm2, _)), T), rep_set_name) =
   10.73        let
   10.74 -        val sg = sign_of thy4;
   10.75 +        val sg = Theory.sign_of thy4;
   10.76          val RepT = T --> Univ_elT;
   10.77          val Rep_name = Sign.intern_const sg ("Rep_" ^ s);
   10.78          val AbsT = Univ_elT --> T;
   10.79 @@ -331,7 +331,7 @@
   10.80  
   10.81          val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
   10.82          val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
   10.83 -          (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
   10.84 +          (cterm_of (Theory.sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
   10.85  
   10.86        in (thy', char_thms' @ char_thms) end;
   10.87  
   10.88 @@ -361,7 +361,7 @@
   10.89  
   10.90      val iso_thms = if length descr = 1 then [] else
   10.91        drop (length newTs, split_conj_thm
   10.92 -        (prove_goalw_cterm [] (cterm_of (sign_of thy5) iso_t) (fn _ =>
   10.93 +        (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
   10.94             [indtac rep_induct 1,
   10.95              REPEAT (rtac TrueI 1),
   10.96              REPEAT (EVERY
   10.97 @@ -397,7 +397,7 @@
   10.98          val rewrites = map mk_meta_eq iso_char_thms;
   10.99          val inj_thms' = map (fn r => r RS injD) inj_thms;
  10.100  
  10.101 -        val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
  10.102 +        val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
  10.103            (HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
  10.104              [indtac induction 1,
  10.105               REPEAT (EVERY
  10.106 @@ -421,7 +421,7 @@
  10.107  
  10.108          val elem_thm = 
  10.109  	    prove_goalw_cterm []
  10.110 -	      (cterm_of (sign_of thy5)
  10.111 +	      (cterm_of (Theory.sign_of thy5)
  10.112  	       (HOLogic.mk_Trueprop (mk_conj ind_concl2)))
  10.113  	      (fn _ =>
  10.114  	       [indtac induction 1,
  10.115 @@ -447,7 +447,7 @@
  10.116        let
  10.117          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
  10.118          val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
  10.119 -      in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
  10.120 +      in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) eqn) (fn _ =>
  10.121          [resolve_tac inj_thms 1,
  10.122           rewrite_goals_tac rewrites,
  10.123           rtac refl 1,
  10.124 @@ -473,7 +473,7 @@
  10.125        let val inj_thms = Scons_inject::(map make_elim
  10.126          ((map (fn r => r RS injD) iso_inj_thms) @
  10.127            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject]))
  10.128 -      in prove_goalw_cterm [] (cterm_of (sign_of thy5) t) (fn _ =>
  10.129 +      in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
  10.130          [rtac iffI 1,
  10.131           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
  10.132           dresolve_tac rep_congs 1, dtac box_equals 1,
  10.133 @@ -504,7 +504,7 @@
  10.134            mk_Free "x" T i;
  10.135  
  10.136          val Abs_t = if i < length newTs then
  10.137 -            Const (Sign.intern_const (sign_of thy6)
  10.138 +            Const (Sign.intern_const (Theory.sign_of thy6)
  10.139                ("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT --> T)
  10.140            else Const (inv_name, [T --> Univ_elT, Univ_elT] ---> T) $
  10.141              Const (nth_elem (i, all_rep_names), T --> Univ_elT)
  10.142 @@ -518,7 +518,7 @@
  10.143      val (indrule_lemma_prems, indrule_lemma_concls) =
  10.144        foldl mk_indrule_lemma (([], []), (descr' ~~ recTs));
  10.145  
  10.146 -    val cert = cterm_of (sign_of thy6);
  10.147 +    val cert = cterm_of (Theory.sign_of thy6);
  10.148  
  10.149      val indrule_lemma = prove_goalw_cterm [] (cert
  10.150        (Logic.mk_implies
    11.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 17 16:53:32 1999 +0100
    11.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 17 16:53:46 1999 +0100
    11.3 @@ -63,8 +63,8 @@
    11.4  (*For simplifying the elimination rule*)
    11.5  val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
    11.6  
    11.7 -val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op -``";
    11.8 -val mono_name = Sign.intern_const (sign_of Ord.thy) "mono";
    11.9 +val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
   11.10 +val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
   11.11  
   11.12  (* make injections needed in mutually recursive definitions *)
   11.13  
   11.14 @@ -225,7 +225,7 @@
   11.15    let
   11.16      val _ = message "  Proving monotonicity...";
   11.17  
   11.18 -    val mono = prove_goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop
   11.19 +    val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   11.20        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   11.21          (fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)])
   11.22  
   11.23 @@ -245,7 +245,7 @@
   11.24        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   11.25  
   11.26      val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
   11.27 -      (cterm_of (sign_of thy) intr) (fn prems =>
   11.28 +      (cterm_of (Theory.sign_of thy) intr) (fn prems =>
   11.29         [(*insert prems and underlying sets*)
   11.30         cut_facts_tac prems 1,
   11.31         stac unfold 1,
   11.32 @@ -272,7 +272,7 @@
   11.33        map make_elim [Inl_inject, Inr_inject];
   11.34  
   11.35      val elims = map (fn t => prove_goalw_cterm rec_sets_defs
   11.36 -      (cterm_of (sign_of thy) t) (fn prems =>
   11.37 +      (cterm_of (Theory.sign_of thy) t) (fn prems =>
   11.38          [cut_facts_tac [hd prems] 1,
   11.39           dtac (unfold RS subst) 1,
   11.40           REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   11.41 @@ -300,7 +300,7 @@
   11.42  
   11.43  (*String s should have the form t:Si where Si is an inductive set*)
   11.44  fun mk_cases elims s =
   11.45 -  let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT))
   11.46 +  let val prem = assume (read_cterm (Thm.sign_of_thm (hd elims)) (s, propT))
   11.47        fun mk_elim rl = rule_by_tactic (con_elim_tac (simpset())) (prem RS rl) 
   11.48  	               |> standard
   11.49    in case find_first is_some (map (try mk_elim) elims) of
   11.50 @@ -315,7 +315,7 @@
   11.51    let
   11.52      val _ = message "  Proving the induction rule...";
   11.53  
   11.54 -    val sign = sign_of thy;
   11.55 +    val sign = Theory.sign_of thy;
   11.56  
   11.57      val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   11.58  
   11.59 @@ -387,8 +387,8 @@
   11.60      val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   11.61      val setT = HOLogic.mk_setT sumT;
   11.62  
   11.63 -    val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp"
   11.64 -      else Sign.intern_const (sign_of Lfp.thy) "lfp";
   11.65 +    val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
   11.66 +      else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
   11.67  
   11.68      val used = foldr add_term_names (intr_ts, []);
   11.69      val [sname, xname] = variantlist (["S", "x"], used);
   11.70 @@ -421,7 +421,7 @@
   11.71      (* add definiton of recursive sets to theory *)
   11.72  
   11.73      val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   11.74 -    val full_rec_name = Sign.full_name (sign_of thy) rec_name;
   11.75 +    val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   11.76  
   11.77      val rec_const = list_comb
   11.78        (Const (full_rec_name, paramTs ---> setT), params);
   11.79 @@ -538,7 +538,7 @@
   11.80      val _ = Theory.requires thy "Inductive"
   11.81        ((if coind then "co" else "") ^ "inductive definitions");
   11.82  
   11.83 -    val sign = sign_of thy;
   11.84 +    val sign = Theory.sign_of thy;
   11.85  
   11.86      (*parameters should agree for all mutually recursive components*)
   11.87      val (_, params) = strip_comb (hd cs);
   11.88 @@ -566,9 +566,9 @@
   11.89  
   11.90  fun add_inductive verbose coind c_strings intr_strings monos con_defs thy =
   11.91    let
   11.92 -    val sign = sign_of thy;
   11.93 -    val cs = map (readtm (sign_of thy) HOLogic.termTVar) c_strings;
   11.94 -    val intr_ts = map (readtm (sign_of thy) propT) intr_strings;
   11.95 +    val sign = Theory.sign_of thy;
   11.96 +    val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings;
   11.97 +    val intr_ts = map (readtm (Theory.sign_of thy) propT) intr_strings;
   11.98  
   11.99      (* the following code ensures that each recursive set *)
  11.100      (* always has the same type in all introduction rules *)
    12.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Mar 17 16:53:32 1999 +0100
    12.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Mar 17 16:53:46 1999 +0100
    12.3 @@ -193,9 +193,7 @@
    12.4  				fs @ map Bound (0 ::(length ls downto 1))));
    12.5      val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
    12.6  		   Logic.mk_equals (Const (fname, dummyT), rhs))
    12.7 -  in
    12.8 -    inferT_axm sign defpair
    12.9 -  end;
   12.10 +  in Theory.inferT_axm sign defpair end;
   12.11  
   12.12  
   12.13  (* find datatypes which contain all datatypes in tnames' *)
   12.14 @@ -212,7 +210,7 @@
   12.15  fun add_primrec_i alt_name eqns_atts thy =
   12.16    let
   12.17      val (eqns, atts) = split_list eqns_atts;
   12.18 -    val sg = sign_of thy;
   12.19 +    val sg = Theory.sign_of thy;
   12.20      val dt_info = DatatypePackage.get_datatypes thy;
   12.21      val rec_eqns = foldr (process_eqn sg) (map snd eqns, []);
   12.22      val tnames = distinct (map (#1 o snd) rec_eqns);
   12.23 @@ -242,7 +240,7 @@
   12.24      val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
   12.25      val _ = writeln ("Proving equations for primrec function(s)\n" ^
   12.26        commas_quote names1 ^ " ...");
   12.27 -    val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
   12.28 +    val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
   12.29          (fn _ => [rtac refl 1])) eqns;
   12.30      val simps = char_thms;
   12.31      val thy'' =
   12.32 @@ -254,7 +252,7 @@
   12.33  
   12.34  
   12.35  fun read_eqn thy ((name, s), srcs) =
   12.36 -  ((name, readtm (sign_of thy) propT s), map (Attrib.global_attribute thy) srcs);
   12.37 +  ((name, readtm (Theory.sign_of thy) propT s), map (Attrib.global_attribute thy) srcs);
   12.38  
   12.39  fun add_primrec alt_name eqns thy = add_primrec_i alt_name (map (read_eqn thy) eqns) thy;
   12.40  
    13.1 --- a/src/HOL/Tools/record_package.ML	Wed Mar 17 16:53:32 1999 +0100
    13.2 +++ b/src/HOL/Tools/record_package.ML	Wed Mar 17 16:53:46 1999 +0100
    13.3 @@ -456,7 +456,7 @@
    13.4  
    13.5  fun field_type_def ((thy, simps), (name, tname, vs, T, U)) =
    13.6    let
    13.7 -    val full = Sign.full_name (sign_of thy);
    13.8 +    val full = Sign.full_name (Theory.sign_of thy);
    13.9      val (thy', {simps = simps', ...}) =
   13.10        thy
   13.11        |> setmp DatatypePackage.quiet_mode true
    14.1 --- a/src/HOL/simpdata.ML	Wed Mar 17 16:53:32 1999 +0100
    14.2 +++ b/src/HOL/simpdata.ML	Wed Mar 17 16:53:46 1999 +0100
    14.3 @@ -315,10 +315,10 @@
    14.4  
    14.5  local
    14.6  val ex_pattern =
    14.7 -  read_cterm (sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
    14.8 +  Thm.read_cterm (Theory.sign_of HOL.thy) ("EX x. P(x) & Q(x)",HOLogic.boolT)
    14.9  
   14.10  val all_pattern =
   14.11 -  read_cterm (sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
   14.12 +  Thm.read_cterm (Theory.sign_of HOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)",HOLogic.boolT)
   14.13  
   14.14  in
   14.15  val defEX_regroup =