accomodate identification of type Sign.sg and theory;
authorwenzelm
Fri Jun 17 18:33:08 2005 +0200 (2005-06-17)
changeset 164252427be27cc60
parent 16424 18a07ad8fea8
child 16426 8c3118c9c054
accomodate identification of type Sign.sg and theory;
TFL/casesplit.ML
src/HOLCF/IOA/Modelcheck/MuIOA.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/drule.ML
src/Pure/tactic.ML
src/Pure/thm.ML
src/Pure/unify.ML
src/ZF/Datatype.ML
     1.1 --- a/TFL/casesplit.ML	Fri Jun 17 18:33:05 2005 +0200
     1.2 +++ b/TFL/casesplit.ML	Fri Jun 17 18:33:08 2005 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4  (* get the case_thm (my version) from a type *)
     1.5  fun case_thm_of_ty sgn ty  = 
     1.6      let 
     1.7 -      val dtypestab = DatatypePackage.get_datatypes_sg sgn;
     1.8 +      val dtypestab = DatatypePackage.get_datatypes sgn;
     1.9        val ty_str = case ty of 
    1.10                       Type(ty_str, _) => ty_str
    1.11                     | TFree(s,_)  => raise ERROR_MESSAGE 
     2.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Fri Jun 17 18:33:05 2005 +0200
     2.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Fri Jun 17 18:33:08 2005 +0200
     2.3 @@ -164,7 +164,7 @@
     2.4  
     2.5  fun mk_sim_oracle (sign, SimOracleExn (subgoal,thl)) =
     2.6  (let
     2.7 -        val weak_case_congs = DatatypePackage.weak_case_congs_of_sg sign;
     2.8 +        val weak_case_congs = DatatypePackage.weak_case_congs_of sign;
     2.9  
    2.10  	val concl = (Logic.strip_imp_concl subgoal);
    2.11  
     3.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jun 17 18:33:05 2005 +0200
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Jun 17 18:33:08 2005 +0200
     3.3 @@ -186,9 +186,8 @@
     3.4    (case assoc_string (kinds, kind) of
     3.5      SOME (intern, check, hide) =>
     3.6        let
     3.7 -        val sg = Theory.sign_of thy;
     3.8 -        val names = if int then map (intern sg) xnames else xnames;
     3.9 -        val bads = filter_out (check sg) names;
    3.10 +        val names = if int then map (intern thy) xnames else xnames;
    3.11 +        val bads = filter_out (check thy) names;
    3.12        in
    3.13          if null bads then hide true names thy
    3.14          else error ("Attempt to hide undeclared item(s): " ^ commas_quote bads)
    3.15 @@ -313,6 +312,8 @@
    3.16  
    3.17  fun pretty_results ctxt ((kind, ""), facts) =
    3.18        Pretty.block (Pretty.str kind :: Pretty.brk 1 :: prt_facts ctxt facts)
    3.19 +  | pretty_results ctxt ((kind, name), [fact]) = Pretty.blk (1,
    3.20 +      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, ProofContext.pretty_fact ctxt fact])
    3.21    | pretty_results ctxt ((kind, name), facts) = Pretty.blk (1,
    3.22        [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk,
    3.23          Pretty.blk (1, Pretty.str "(" :: prt_facts ctxt facts @ [Pretty.str ")"])]);
    3.24 @@ -385,8 +386,8 @@
    3.25  fun locale_multi_theorem k locale (name, atts) elems concl int thy =
    3.26    global_statement (Proof.multi_theorem k I  ProofContext.export_standard
    3.27        (SOME (locale,
    3.28 -        (map (Attrib.intern_src (Theory.sign_of thy)) atts,
    3.29 -         map (map (Attrib.intern_src (Theory.sign_of thy)) o snd o fst) concl)))
    3.30 +        (map (Attrib.intern_src thy) atts,
    3.31 +         map (map (Attrib.intern_src thy) o snd o fst) concl)))
    3.32        (name, [])
    3.33        (map (Locale.intern_attrib_elem_expr thy) elems))
    3.34      (map (apfst (apsnd (K []))) concl) int thy;
    3.35 @@ -554,7 +555,7 @@
    3.36  (* translation functions *)
    3.37  
    3.38  fun advancedT false = ""
    3.39 -  | advancedT true = "Sign.sg -> ";
    3.40 +  | advancedT true = "theory -> ";
    3.41  
    3.42  fun advancedN false = ""
    3.43    | advancedN true = "advanced_";
    3.44 @@ -610,7 +611,7 @@
    3.45  
    3.46  fun add_oracle (name, txt) =
    3.47    Context.use_let
    3.48 -    "val oracle: bstring * (Sign.sg * Object.T -> term)"
    3.49 +    "val oracle: bstring * (theory * Object.T -> term)"
    3.50      "Theory.add_oracle oracle"
    3.51      ("(" ^ Library.quote name ^ ", " ^ txt ^ ")");
    3.52  
    3.53 @@ -635,8 +636,8 @@
    3.54    in
    3.55      multi_theorem_i Drule.internalK activate ProofContext.export_plain
    3.56        ("", []) []
    3.57 -      (map (fn ((n, ps), props) => 
    3.58 -          ((NameSpace.base n, [witness (n, map Logic.varify ps)]), 
    3.59 +      (map (fn ((n, ps), props) =>
    3.60 +          ((NameSpace.base n, [witness (n, map Logic.varify ps)]),
    3.61          map (fn prop => (prop, ([], []))) props)) propss) int thy'
    3.62    end;
    3.63  
    3.64 @@ -659,16 +660,20 @@
    3.65  (* theory init and exit *)
    3.66  
    3.67  fun gen_begin_theory upd name parents files =
    3.68 -  let val ml_filename = Path.pack (ThyLoad.ml_path name);
    3.69 -      val () = if exists (equal ml_filename o #1) files
    3.70 -               then error ((quote ml_filename) ^ " not allowed in files section for theory " ^ name)
    3.71 -               else ()
    3.72 -  in ThyInfo.begin_theory Present.begin_theory upd name parents (map (apfst Path.unpack) files) end;
    3.73 +  let
    3.74 +    val ml_filename = Path.pack (ThyLoad.ml_path name);
    3.75 +    (* FIXME unreliable test -- better make ThyInfo manage dependencies properly *)
    3.76 +    val _ = conditional (exists (equal ml_filename o #1) files) (fn () =>
    3.77 +      error ((quote ml_filename) ^ " not allowed in files section for theory " ^ name));
    3.78 +  in
    3.79 +    ThyInfo.begin_theory Present.begin_theory upd name parents
    3.80 +      (map (apfst Path.unpack) files)
    3.81 +  end;
    3.82  
    3.83  val begin_theory = gen_begin_theory false;
    3.84  
    3.85  fun end_theory thy =
    3.86 -  if ThyInfo.check_known_thy (PureThy.get_name thy) then ThyInfo.end_theory thy
    3.87 +  if ThyInfo.check_known_thy (Context.theory_name thy) then ThyInfo.end_theory thy
    3.88    else thy;
    3.89  
    3.90  val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
    3.91 @@ -677,7 +682,8 @@
    3.92  fun bg_theory (name, parents, files) int = gen_begin_theory int name parents files;
    3.93  fun en_theory thy = (end_theory thy; ());
    3.94  
    3.95 -fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o PureThy.get_name);
    3.96 +fun theory spec =
    3.97 +  Toplevel.init_theory (bg_theory spec) en_theory (kill_theory o Context.theory_name);
    3.98  
    3.99  
   3.100  (* context switch *)
     4.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Jun 17 18:33:05 2005 +0200
     4.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Jun 17 18:33:08 2005 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  signature PROOF_SYNTAX =
     4.5  sig
     4.6    val proofT : typ
     4.7 -  val add_proof_syntax : Sign.sg -> Sign.sg
     4.8 +  val add_proof_syntax : theory -> theory
     4.9    val disambiguate_names : theory -> Proofterm.proof ->
    4.10      Proofterm.proof * Proofterm.proof Symtab.table
    4.11    val proof_of_term : theory -> Proofterm.proof Symtab.table ->
    4.12 @@ -17,7 +17,7 @@
    4.13    val cterm_of_proof : theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
    4.14    val read_term : theory -> typ -> string -> term
    4.15    val read_proof : theory -> bool -> string -> Proofterm.proof
    4.16 -  val pretty_proof : Sign.sg -> Proofterm.proof -> Pretty.T
    4.17 +  val pretty_proof : theory -> Proofterm.proof -> Pretty.T
    4.18    val pretty_proof_of : bool -> thm -> Pretty.T
    4.19    val print_proof_of : bool -> thm -> unit
    4.20  end;
    4.21 @@ -37,20 +37,20 @@
    4.22  
    4.23  (** constants for theorems and axioms **)
    4.24  
    4.25 -fun add_proof_atom_consts names sg =
    4.26 -  sg
    4.27 -  |> Sign.add_path "//"
    4.28 -  |> Sign.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
    4.29 +fun add_proof_atom_consts names thy =
    4.30 +  thy
    4.31 +  |> Theory.absolute_path
    4.32 +  |> Theory.add_consts_i (map (fn name => (name, proofT, NoSyn)) names);
    4.33  
    4.34  (** constants for application and abstraction **)
    4.35  
    4.36 -fun add_proof_syntax sg =
    4.37 -  sg
    4.38 -  |> Sign.copy
    4.39 -  |> Sign.add_path "/"
    4.40 -  |> Sign.add_defsort_i []
    4.41 -  |> Sign.add_types [("proof", 0, NoSyn)]
    4.42 -  |> Sign.add_consts_i
    4.43 +fun add_proof_syntax thy =
    4.44 +  thy
    4.45 +  |> Theory.copy
    4.46 +  |> Theory.root_path
    4.47 +  |> Theory.add_defsort_i []
    4.48 +  |> Theory.add_types [("proof", 0, NoSyn)]
    4.49 +  |> Theory.add_consts_i
    4.50        [("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ %/ _)", [4, 5], 4)),
    4.51         ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ %%/ _)", [4, 5], 4)),
    4.52         ("Abst", (aT --> proofT) --> proofT, NoSyn),
    4.53 @@ -58,8 +58,8 @@
    4.54         ("Hyp", propT --> proofT, NoSyn),
    4.55         ("Oracle", propT --> proofT, NoSyn),
    4.56         ("MinProof", proofT, Delimfix "?")]
    4.57 -  |> Sign.add_nonterminals ["param", "params"]
    4.58 -  |> Sign.add_syntax_i
    4.59 +  |> Theory.add_nonterminals ["param", "params"]
    4.60 +  |> Theory.add_syntax_i
    4.61        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
    4.62         ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    4.63         ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    4.64 @@ -67,13 +67,13 @@
    4.65         ("", paramT --> paramT, Delimfix "'(_')"),
    4.66         ("", idtT --> paramsT, Delimfix "_"),
    4.67         ("", paramT --> paramsT, Delimfix "_")]
    4.68 -  |> Sign.add_modesyntax_i (("xsymbols", true),
    4.69 +  |> Theory.add_modesyntax_i ("xsymbols", true)
    4.70        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<Lambda>_./ _)", [0, 3], 3)),
    4.71         ("Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \\<cdot>/ _)", [4, 5], 4)),
    4.72 -       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))])
    4.73 -  |> Sign.add_modesyntax_i (("latex", false),
    4.74 -      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))])
    4.75 -  |> Sign.add_trrules_i (map Syntax.ParsePrintRule
    4.76 +       ("AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \\<bullet>/ _)", [4, 5], 4))]
    4.77 +  |> Theory.add_modesyntax_i ("latex", false)
    4.78 +      [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\\<^bold>\\<lambda>_./ _)", [0, 3], 3))]
    4.79 +  |> Theory.add_trrules_i (map Syntax.ParsePrintRule
    4.80        [(Syntax.mk_appl (Constant "_Lam")
    4.81            [Syntax.mk_appl (Constant "_Lam0") [Variable "l", Variable "m"], Variable "A"],
    4.82          Syntax.mk_appl (Constant "_Lam")
    4.83 @@ -167,7 +167,7 @@
    4.84        | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
    4.85            (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t))
    4.86        | prf_of _ t = error ("Not a proof term:\n" ^
    4.87 -          Sign.string_of_term (sign_of thy) t)
    4.88 +          Sign.string_of_term thy t)
    4.89  
    4.90    in prf_of [] end;
    4.91  
    4.92 @@ -217,12 +217,12 @@
    4.93      val thm_names = filter_out (equal "")
    4.94        (map fst (PureThy.all_thms_of thy) @ map fst (Symtab.dest tab));
    4.95      val axm_names = map fst (Theory.all_axioms_of thy);
    4.96 -    val sg = sign_of thy |>
    4.97 -      add_proof_syntax |>
    4.98 -      add_proof_atom_consts
    4.99 +    val thy' = thy
   4.100 +      |> add_proof_syntax
   4.101 +      |> add_proof_atom_consts
   4.102          (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
   4.103    in
   4.104 -    (cterm_of sg (term_of_proof prf'),
   4.105 +    (cterm_of thy' (term_of_proof prf'),
   4.106       proof_of_term thy tab true o Thm.term_of)
   4.107    end;
   4.108  
   4.109 @@ -230,12 +230,12 @@
   4.110    let
   4.111      val thm_names = filter_out (equal "") (map fst (PureThy.all_thms_of thy));
   4.112      val axm_names = map fst (Theory.all_axioms_of thy);
   4.113 -    val sg = sign_of thy |>
   4.114 -      add_proof_syntax |>
   4.115 -      add_proof_atom_consts
   4.116 +    val thy' = thy
   4.117 +      |> add_proof_syntax
   4.118 +      |> add_proof_atom_consts
   4.119          (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
   4.120    in
   4.121 -    (fn T => fn s => Thm.term_of (read_cterm sg (s, T)))
   4.122 +    fn T => fn s => Thm.term_of (read_cterm thy' (s, T))
   4.123    end;
   4.124  
   4.125  fun read_proof thy =
   4.126 @@ -244,27 +244,27 @@
   4.127      (fn ty => fn s => proof_of_term thy Symtab.empty ty (Logic.varify (rd s)))
   4.128    end;
   4.129  
   4.130 -fun pretty_proof sg prf =
   4.131 +fun pretty_proof thy prf =
   4.132    let
   4.133      val thm_names = map fst (Symtab.dest (thms_of_proof Symtab.empty prf)) \ "";
   4.134      val axm_names = map fst (Symtab.dest (axms_of_proof Symtab.empty prf));
   4.135 -    val sg' = sg |>
   4.136 +    val thy' = thy |>
   4.137        add_proof_syntax |>
   4.138        add_proof_atom_consts
   4.139          (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names)
   4.140    in
   4.141 -    Sign.pretty_term sg' (term_of_proof prf)
   4.142 +    Sign.pretty_term thy' (term_of_proof prf)
   4.143    end;
   4.144  
   4.145  fun pretty_proof_of full thm =
   4.146    let
   4.147 -    val {sign, der = (_, prf), prop, ...} = rep_thm thm;
   4.148 +    val {thy, der = (_, prf), prop, ...} = rep_thm thm;
   4.149      val prf' = (case strip_combt (fst (strip_combP prf)) of
   4.150          (PThm (_, prf', prop', _), _) => if prop=prop' then prf' else prf
   4.151        | _ => prf)
   4.152    in
   4.153 -    pretty_proof sign
   4.154 -      (if full then Reconstruct.reconstruct_proof sign prop prf' else prf')
   4.155 +    pretty_proof thy
   4.156 +      (if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
   4.157    end;
   4.158  
   4.159  val print_proof_of = Pretty.writeln oo pretty_proof_of;
     5.1 --- a/src/Pure/drule.ML	Fri Jun 17 18:33:05 2005 +0200
     5.2 +++ b/src/Pure/drule.ML	Fri Jun 17 18:33:08 2005 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4    val cterm_fun         : (term -> term) -> (cterm -> cterm)
     5.5    val ctyp_fun          : (typ -> typ) -> (ctyp -> ctyp)
     5.6    val read_insts        :
     5.7 -          Sign.sg -> (indexname -> typ option) * (indexname -> sort option)
     5.8 +          theory -> (indexname -> typ option) * (indexname -> sort option)
     5.9                    -> (indexname -> typ option) * (indexname -> sort option)
    5.10                    -> string list -> (indexname * string) list
    5.11                    -> (ctyp * ctyp) list * (cterm * cterm) list
    5.12 @@ -54,10 +54,10 @@
    5.13    val OF                : thm * thm list -> thm
    5.14    val compose           : thm * int * thm -> thm list
    5.15    val COMP              : thm * thm -> thm
    5.16 -  val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
    5.17 +  val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
    5.18    val read_instantiate  : (string*string)list -> thm -> thm
    5.19    val cterm_instantiate : (cterm*cterm)list -> thm -> thm
    5.20 -  val eq_thm_sg         : thm * thm -> bool
    5.21 +  val eq_thm_thy        : thm * thm -> bool
    5.22    val eq_thm_prop	: thm * thm -> bool
    5.23    val weak_eq_thm       : thm * thm -> bool
    5.24    val size_of_thm       : thm -> int
    5.25 @@ -123,7 +123,7 @@
    5.26    val fconv_rule        : (cterm -> thm) -> thm -> thm
    5.27    val norm_hhf_eq: thm
    5.28    val is_norm_hhf: term -> bool
    5.29 -  val norm_hhf: Sign.sg -> term -> term
    5.30 +  val norm_hhf: theory -> term -> term
    5.31    val triv_goal: thm
    5.32    val rev_triv_goal: thm
    5.33    val implies_intr_goals: cterm list -> thm -> thm
    5.34 @@ -146,7 +146,7 @@
    5.35    val conj_elim_precise: int -> thm -> thm list
    5.36    val conj_intr_thm: thm
    5.37    val abs_def: thm -> thm
    5.38 -  val read_instantiate_sg': Sign.sg -> (indexname * string) list -> thm -> thm
    5.39 +  val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
    5.40    val read_instantiate': (indexname * string) list -> thm -> thm
    5.41  end;
    5.42  
    5.43 @@ -190,16 +190,14 @@
    5.44  val cprems_of = strip_imp_prems o cprop_of;
    5.45  
    5.46  fun cterm_fun f ct =
    5.47 -  let val {t, sign, ...} = Thm.rep_cterm ct
    5.48 -  in Thm.cterm_of sign (f t) end;
    5.49 +  let val {t, thy, ...} = Thm.rep_cterm ct
    5.50 +  in Thm.cterm_of thy (f t) end;
    5.51  
    5.52  fun ctyp_fun f cT =
    5.53 -  let val {T, sign, ...} = Thm.rep_ctyp cT
    5.54 -  in Thm.ctyp_of sign (f T) end;
    5.55 +  let val {T, thy, ...} = Thm.rep_ctyp cT
    5.56 +  in Thm.ctyp_of thy (f T) end;
    5.57  
    5.58 -val proto_sign = Theory.sign_of ProtoPure.thy;
    5.59 -
    5.60 -val implies = cterm_of proto_sign Term.implies;
    5.61 +val implies = cterm_of ProtoPure.thy Term.implies;
    5.62  
    5.63  (*cterm version of mk_implies*)
    5.64  fun mk_implies(A,B) = Thm.capply (Thm.capply implies A) B;
    5.65 @@ -259,7 +257,7 @@
    5.66  fun inst_failure ixn =
    5.67    error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
    5.68  
    5.69 -fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
    5.70 +fun read_insts thy (rtypes,rsorts) (types,sorts) used insts =
    5.71  let
    5.72      fun is_tv ((a, _), _) =
    5.73        (case Symbol.explode a of "'" :: _ => true | _ => false);
    5.74 @@ -267,8 +265,8 @@
    5.75      fun sort_of ixn = case rsorts ixn of SOME S => S | NONE => absent ixn;
    5.76      fun readT (ixn, st) =
    5.77          let val S = sort_of ixn;
    5.78 -            val T = Sign.read_typ (sign,sorts) st;
    5.79 -        in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
    5.80 +            val T = Sign.read_typ (thy,sorts) st;
    5.81 +        in if Sign.typ_instance thy (T, TVar(ixn,S)) then (ixn,T)
    5.82             else inst_failure ixn
    5.83          end
    5.84      val tye = map readT tvs;
    5.85 @@ -278,13 +276,13 @@
    5.86      val ixnsTs = map mkty vs;
    5.87      val ixns = map fst ixnsTs
    5.88      and sTs  = map snd ixnsTs
    5.89 -    val (cts,tye2) = read_def_cterms(sign,types,sorts) used false sTs;
    5.90 +    val (cts,tye2) = read_def_cterms(thy,types,sorts) used false sTs;
    5.91      fun mkcVar(ixn,T) =
    5.92          let val U = typ_subst_TVars tye2 T
    5.93 -        in cterm_of sign (Var(ixn,U)) end
    5.94 +        in cterm_of thy (Var(ixn,U)) end
    5.95      val ixnTs = ListPair.zip(ixns, map snd sTs)
    5.96 -in (map (fn (ixn, T) => (ctyp_of sign (TVar (ixn, sort_of ixn)),
    5.97 -      ctyp_of sign T)) (tye2 @ tye),
    5.98 +in (map (fn (ixn, T) => (ctyp_of thy (TVar (ixn, sort_of ixn)),
    5.99 +      ctyp_of thy T)) (tye2 @ tye),
   5.100      ListPair.zip(map mkcVar ixnTs,cts))
   5.101  end;
   5.102  
   5.103 @@ -362,7 +360,7 @@
   5.104  (*Strip extraneous shyps as far as possible*)
   5.105  fun strip_shyps_warning thm =
   5.106    let
   5.107 -    val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.sign_of_thm thm);
   5.108 +    val str_of_sort = Pretty.str_of o Sign.pretty_sort (Thm.theory_of_thm thm);
   5.109      val thm' = Thm.strip_shyps thm;
   5.110      val xshyps = Thm.extra_shyps thm';
   5.111    in
   5.112 @@ -379,9 +377,9 @@
   5.113  
   5.114  (*Generalization over all suitable Free variables*)
   5.115  fun forall_intr_frees th =
   5.116 -    let val {prop,sign,...} = rep_thm th
   5.117 +    let val {prop,thy,...} = rep_thm th
   5.118      in  forall_intr_list
   5.119 -         (map (cterm_of sign) (sort (make_ord atless) (term_frees prop)))
   5.120 +         (map (cterm_of thy) (sort (make_ord atless) (term_frees prop)))
   5.121           th
   5.122      end;
   5.123  
   5.124 @@ -390,8 +388,8 @@
   5.125  
   5.126  fun gen_all thm =
   5.127    let
   5.128 -    val {sign, prop, maxidx, ...} = Thm.rep_thm thm;
   5.129 -    fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of sign (Var ((x, maxidx + 1), T))) th;
   5.130 +    val {thy, prop, maxidx, ...} = Thm.rep_thm thm;
   5.131 +    fun elim (th, (x, T)) = Thm.forall_elim (Thm.cterm_of thy (Var ((x, maxidx + 1), T))) th;
   5.132      val vs = Term.strip_all_vars prop;
   5.133    in Library.foldl elim (thm, Term.variantlist (map #1 vs, []) ~~ map #2 vs) end;
   5.134  
   5.135 @@ -415,7 +413,7 @@
   5.136  
   5.137  (*Reset Var indexes to zero, renaming to preserve distinctness*)
   5.138  fun zero_var_indexes th =
   5.139 -    let val {prop,sign,tpairs,...} = rep_thm th;
   5.140 +    let val {prop,thy,tpairs,...} = rep_thm th;
   5.141          val (tpair_l, tpair_r) = Library.split_list tpairs;
   5.142          val vars = foldr add_term_vars 
   5.143                           (foldr add_term_vars (term_vars prop) tpair_l) tpair_r;
   5.144 @@ -426,12 +424,12 @@
   5.145          val nms' = rev(Library.foldl add_new_id ([], map (#1 o #1) inrs));
   5.146          val tye = ListPair.map (fn ((v, rs), a) => (TVar (v, rs), TVar ((a, 0), rs)))
   5.147                       (inrs, nms')
   5.148 -        val ctye = map (pairself (ctyp_of sign)) tye;
   5.149 +        val ctye = map (pairself (ctyp_of thy)) tye;
   5.150          fun varpairs([],[]) = []
   5.151            | varpairs((var as Var(v,T)) :: vars, b::bs) =
   5.152                  let val T' = typ_subst_atomic tye T
   5.153 -                in (cterm_of sign (Var(v,T')),
   5.154 -                    cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs)
   5.155 +                in (cterm_of thy (Var(v,T')),
   5.156 +                    cterm_of thy (Var((b,0),T'))) :: varpairs(vars,bs)
   5.157                  end
   5.158            | varpairs _ = raise TERM("varpairs", []);
   5.159      in Thm.instantiate (ctye, varpairs(vars,rev bs)) th end;
   5.160 @@ -474,7 +472,7 @@
   5.161  
   5.162  fun freeze_thaw_robust th =
   5.163   let val fth = freezeT th
   5.164 -     val {prop, tpairs, sign, ...} = rep_thm fth
   5.165 +     val {prop, tpairs, thy, ...} = rep_thm fth
   5.166   in
   5.167     case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   5.168         [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
   5.169 @@ -484,8 +482,8 @@
   5.170                     in  ((ix,v)::pairs)  end;
   5.171               val alist = foldr newName [] vars
   5.172               fun mk_inst (Var(v,T)) =
   5.173 -                 (cterm_of sign (Var(v,T)),
   5.174 -                  cterm_of sign (Free(valOf (assoc(alist,v)), T)))
   5.175 +                 (cterm_of thy (Var(v,T)),
   5.176 +                  cterm_of thy (Free(valOf (assoc(alist,v)), T)))
   5.177               val insts = map mk_inst vars
   5.178               fun thaw i th' = (*i is non-negative increment for Var indexes*)
   5.179                   th' |> forall_intr_list (map #2 insts)
   5.180 @@ -497,7 +495,7 @@
   5.181    The Frees created from Vars have nice names.*)
   5.182  fun freeze_thaw th =
   5.183   let val fth = freezeT th
   5.184 -     val {prop, tpairs, sign, ...} = rep_thm fth
   5.185 +     val {prop, tpairs, thy, ...} = rep_thm fth
   5.186   in
   5.187     case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
   5.188         [] => (fth, fn x => x)
   5.189 @@ -508,8 +506,8 @@
   5.190               val (alist, _) = foldr newName ([], Library.foldr add_term_names
   5.191                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars
   5.192               fun mk_inst (Var(v,T)) =
   5.193 -                 (cterm_of sign (Var(v,T)),
   5.194 -                  cterm_of sign (Free(valOf (assoc(alist,v)), T)))
   5.195 +                 (cterm_of thy (Var(v,T)),
   5.196 +                  cterm_of thy (Free(valOf (assoc(alist,v)), T)))
   5.197               val insts = map mk_inst vars
   5.198               fun thaw th' =
   5.199                   th' |> forall_intr_list (map #2 insts)
   5.200 @@ -536,9 +534,8 @@
   5.201    Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |]
   5.202               [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ]    *)
   5.203  fun assume_ax thy sP =
   5.204 -    let val sign = Theory.sign_of thy
   5.205 -        val prop = Logic.close_form (term_of (read_cterm sign (sP, propT)))
   5.206 -    in forall_elim_vars 0 (assume (cterm_of sign prop))  end;
   5.207 +  let val prop = Logic.close_form (term_of (read_cterm thy (sP, propT)))
   5.208 +  in forall_elim_vars 0 (Thm.assume (cterm_of thy prop)) end;
   5.209  
   5.210  (*Resolution: exactly one resolvent must be produced.*)
   5.211  fun tha RSN (i,thb) =
   5.212 @@ -594,8 +591,8 @@
   5.213  
   5.214  (** theorem equality **)
   5.215  
   5.216 -(*True if the two theorems have the same signature.*)
   5.217 -val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
   5.218 +(*True if the two theorems have the same theory.*)
   5.219 +val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm;
   5.220  
   5.221  (*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
   5.222  val eq_thm_prop = op aconv o pairself Thm.prop_of;
   5.223 @@ -622,16 +619,16 @@
   5.224    | term_vars' _ = [];
   5.225  
   5.226  fun forall_intr_vars th =
   5.227 -  let val {prop,sign,...} = rep_thm th;
   5.228 +  let val {prop,thy,...} = rep_thm th;
   5.229        val vars = distinct (term_vars' prop);
   5.230 -  in forall_intr_list (map (cterm_of sign) vars) th end;
   5.231 +  in forall_intr_list (map (cterm_of thy) vars) th end;
   5.232  
   5.233  val weak_eq_thm = Thm.eq_thm o pairself (forall_intr_vars o freezeT);
   5.234  
   5.235  
   5.236  (*** Meta-Rewriting Rules ***)
   5.237  
   5.238 -fun read_prop s = read_cterm proto_sign (s, propT);
   5.239 +fun read_prop s = read_cterm ProtoPure.thy (s, propT);
   5.240  
   5.241  fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
   5.242  fun store_standard_thm name thm = store_thm name (standard thm);
   5.243 @@ -639,7 +636,7 @@
   5.244  fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
   5.245  
   5.246  val reflexive_thm =
   5.247 -  let val cx = cterm_of proto_sign (Var(("x",0),TVar(("'a",0),[])))
   5.248 +  let val cx = cterm_of ProtoPure.thy (Var(("x",0),TVar(("'a",0),[])))
   5.249    in store_standard_thm_open "reflexive" (Thm.reflexive cx) end;
   5.250  
   5.251  val symmetric_thm =
   5.252 @@ -768,7 +765,7 @@
   5.253  val triv_forall_equality =
   5.254    let val V  = read_prop "PROP V"
   5.255        and QV = read_prop "!!x::'a. PROP V"
   5.256 -      and x  = read_cterm proto_sign ("x", TypeInfer.logicT);
   5.257 +      and x  = read_cterm ProtoPure.thy ("x", TypeInfer.logicT);
   5.258    in
   5.259      store_standard_thm_open "triv_forall_equality"
   5.260        (equal_intr (implies_intr QV (forall_elim x (assume QV)))
   5.261 @@ -823,7 +820,7 @@
   5.262  
   5.263  val norm_hhf_eq =
   5.264    let
   5.265 -    val cert = Thm.cterm_of proto_sign;
   5.266 +    val cert = Thm.cterm_of ProtoPure.thy;
   5.267      val aT = TFree ("'a", []);
   5.268      val all = Term.all aT;
   5.269      val x = Free ("x", aT);
   5.270 @@ -857,53 +854,53 @@
   5.271        | is_norm _ = true;
   5.272    in is_norm (Pattern.beta_eta_contract tm) end;
   5.273  
   5.274 -fun norm_hhf sg t =
   5.275 +fun norm_hhf thy t =
   5.276    if is_norm_hhf t then t
   5.277 -  else Pattern.rewrite_term (Sign.tsig_of sg) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
   5.278 +  else Pattern.rewrite_term (Sign.tsig_of thy) [Logic.dest_equals (prop_of norm_hhf_eq)] [] t;
   5.279  
   5.280  
   5.281 -(*** Instantiate theorem th, reading instantiations under signature sg ****)
   5.282 +(*** Instantiate theorem th, reading instantiations in theory thy ****)
   5.283  
   5.284  (*Version that normalizes the result: Thm.instantiate no longer does that*)
   5.285  fun instantiate instpair th = Thm.instantiate instpair th  COMP   asm_rl;
   5.286  
   5.287 -fun read_instantiate_sg' sg sinsts th =
   5.288 +fun read_instantiate_sg' thy sinsts th =
   5.289      let val ts = types_sorts th;
   5.290          val used = add_used th [];
   5.291 -    in  instantiate (read_insts sg ts ts used sinsts) th  end;
   5.292 +    in  instantiate (read_insts thy ts ts used sinsts) th  end;
   5.293  
   5.294 -fun read_instantiate_sg sg sinsts th =
   5.295 -  read_instantiate_sg' sg (map (apfst Syntax.indexname) sinsts) th;
   5.296 +fun read_instantiate_sg thy sinsts th =
   5.297 +  read_instantiate_sg' thy (map (apfst Syntax.indexname) sinsts) th;
   5.298  
   5.299  (*Instantiate theorem th, reading instantiations under theory of th*)
   5.300  fun read_instantiate sinsts th =
   5.301 -    read_instantiate_sg (Thm.sign_of_thm th) sinsts th;
   5.302 +    read_instantiate_sg (Thm.theory_of_thm th) sinsts th;
   5.303  
   5.304  fun read_instantiate' sinsts th =
   5.305 -    read_instantiate_sg' (Thm.sign_of_thm th) sinsts th;
   5.306 +    read_instantiate_sg' (Thm.theory_of_thm th) sinsts th;
   5.307  
   5.308  
   5.309  (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
   5.310    Instantiates distinct Vars by terms, inferring type instantiations. *)
   5.311  local
   5.312 -  fun add_types ((ct,cu), (sign,tye,maxidx)) =
   5.313 -    let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   5.314 -        and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   5.315 +  fun add_types ((ct,cu), (thy,tye,maxidx)) =
   5.316 +    let val {thy=thyt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
   5.317 +        and {thy=thyu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
   5.318          val maxi = Int.max(maxidx, Int.max(maxt, maxu));
   5.319 -        val sign' = Sign.merge(sign, Sign.merge(signt, signu))
   5.320 -        val (tye',maxi') = Type.unify (Sign.tsig_of sign') (tye, maxi) (T, U)
   5.321 +        val thy' = Theory.merge(thy, Theory.merge(thyt, thyu))
   5.322 +        val (tye',maxi') = Type.unify (Sign.tsig_of thy') (tye, maxi) (T, U)
   5.323            handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
   5.324 -    in  (sign', tye', maxi')  end;
   5.325 +    in  (thy', tye', maxi')  end;
   5.326  in
   5.327  fun cterm_instantiate ctpairs0 th =
   5.328 -  let val (sign,tye,_) = foldr add_types (Thm.sign_of_thm th, Vartab.empty, 0) ctpairs0
   5.329 +  let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
   5.330        fun instT(ct,cu) = 
   5.331 -        let val inst = cterm_of sign o Envir.subst_TVars tye o term_of
   5.332 +        let val inst = cterm_of thy o Envir.subst_TVars tye o term_of
   5.333          in (inst ct, inst cu) end
   5.334 -      fun ctyp2 (ixn, (S, T)) = (ctyp_of sign (TVar (ixn, S)), ctyp_of sign T)
   5.335 +      fun ctyp2 (ixn, (S, T)) = (ctyp_of thy (TVar (ixn, S)), ctyp_of thy T)
   5.336    in  instantiate (map ctyp2 (Vartab.dest tye), map instT ctpairs0) th  end
   5.337    handle TERM _ =>
   5.338 -           raise THM("cterm_instantiate: incompatible signatures",0,[th])
   5.339 +           raise THM("cterm_instantiate: incompatible theories",0,[th])
   5.340         | TYPE (msg, _, _) => raise THM(msg, 0, [th])
   5.341  end;
   5.342  
   5.343 @@ -912,11 +909,11 @@
   5.344  
   5.345  (*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
   5.346  fun equal_abs_elim ca eqth =
   5.347 -  let val {sign=signa, t=a, ...} = rep_cterm ca
   5.348 +  let val {thy=thya, t=a, ...} = rep_cterm ca
   5.349        and combth = combination eqth (reflexive ca)
   5.350 -      val {sign,prop,...} = rep_thm eqth
   5.351 +      val {thy,prop,...} = rep_thm eqth
   5.352        val (abst,absu) = Logic.dest_equals prop
   5.353 -      val cterm = cterm_of (Sign.merge (sign,signa))
   5.354 +      val cterm = cterm_of (Theory.merge (thy,thya))
   5.355    in  transitive (symmetric (beta_conversion false (cterm (abst$a))))
   5.356             (transitive combth (beta_conversion false (cterm (absu$a))))
   5.357    end
   5.358 @@ -929,7 +926,7 @@
   5.359  (*** Goal (PROP A) <==> PROP A ***)
   5.360  
   5.361  local
   5.362 -  val cert = Thm.cterm_of proto_sign;
   5.363 +  val cert = Thm.cterm_of ProtoPure.thy;
   5.364    val A = Free ("A", propT);
   5.365    val G = Logic.mk_goal A;
   5.366    val (G_def, _) = freeze_thaw ProtoPure.Goal_def;
   5.367 @@ -940,7 +937,7 @@
   5.368        (Thm.equal_elim G_def (Thm.assume (cert G)))));
   5.369  end;
   5.370  
   5.371 -val mk_cgoal = Thm.capply (Thm.cterm_of proto_sign Logic.goal_const);
   5.372 +val mk_cgoal = Thm.capply (Thm.cterm_of ProtoPure.thy Logic.goal_const);
   5.373  fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal;
   5.374  
   5.375  fun implies_intr_goals cprops thm =
   5.376 @@ -952,7 +949,7 @@
   5.377  (** variations on instantiate **)
   5.378  
   5.379  (*shorthand for instantiating just one variable in the current theory*)
   5.380 -fun inst x t = read_instantiate_sg (sign_of (the_context())) [(x,t)];
   5.381 +fun inst x t = read_instantiate_sg (the_context()) [(x,t)];
   5.382  
   5.383  
   5.384  (* collect vars in left-to-right order *)
   5.385 @@ -974,11 +971,11 @@
   5.386          List.mapPartial (Option.map Thm.term_of) cts);
   5.387  
   5.388      fun inst_of (v, ct) =
   5.389 -      (Thm.cterm_of (#sign (Thm.rep_cterm ct)) (Var v), ct)
   5.390 +      (Thm.cterm_of (Thm.theory_of_cterm ct) (Var v), ct)
   5.391          handle TYPE (msg, _, _) => err msg;
   5.392  
   5.393      fun tyinst_of (v, cT) =
   5.394 -      (Thm.ctyp_of (#sign (Thm.rep_ctyp cT)) (TVar v), cT)
   5.395 +      (Thm.ctyp_of (Thm.theory_of_ctyp cT) (TVar v), cT)
   5.396          handle TYPE (msg, _, _) => err msg;
   5.397  
   5.398      fun zip_vars _ [] = []
   5.399 @@ -1005,18 +1002,18 @@
   5.400  fun rename_bvars [] thm = thm
   5.401    | rename_bvars vs thm =
   5.402      let
   5.403 -      val {sign, prop, ...} = rep_thm thm;
   5.404 +      val {thy, prop, ...} = rep_thm thm;
   5.405        fun ren (Abs (x, T, t)) = Abs (getOpt (assoc (vs, x), x), T, ren t)
   5.406          | ren (t $ u) = ren t $ ren u
   5.407          | ren t = t;
   5.408 -    in equal_elim (reflexive (cterm_of sign (ren prop))) thm end;
   5.409 +    in equal_elim (reflexive (cterm_of thy (ren prop))) thm end;
   5.410  
   5.411  
   5.412  (* renaming in left-to-right order *)
   5.413  
   5.414  fun rename_bvars' xs thm =
   5.415    let
   5.416 -    val {sign, prop, ...} = rep_thm thm;
   5.417 +    val {thy, prop, ...} = rep_thm thm;
   5.418      fun rename [] t = ([], t)
   5.419        | rename (x' :: xs) (Abs (x, T, t)) =
   5.420            let val (xs', t') = rename xs t
   5.421 @@ -1028,7 +1025,7 @@
   5.422            in (xs'', t' $ u') end
   5.423        | rename xs t = (xs, t);
   5.424    in case rename xs prop of
   5.425 -      ([], prop') => equal_elim (reflexive (cterm_of sign prop')) thm
   5.426 +      ([], prop') => equal_elim (reflexive (cterm_of thy prop')) thm
   5.427      | _ => error "More names than abstractions in theorem"
   5.428    end;
   5.429  
   5.430 @@ -1040,14 +1037,14 @@
   5.431  
   5.432  fun unvarifyT thm =
   5.433    let
   5.434 -    val cT = Thm.ctyp_of (Thm.sign_of_thm thm);
   5.435 +    val cT = Thm.ctyp_of (Thm.theory_of_thm thm);
   5.436      val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (tvars_of thm);
   5.437    in instantiate' tfrees [] thm end;
   5.438  
   5.439  fun unvarify raw_thm =
   5.440    let
   5.441      val thm = unvarifyT raw_thm;
   5.442 -    val ct = Thm.cterm_of (Thm.sign_of_thm thm);
   5.443 +    val ct = Thm.cterm_of (Thm.theory_of_thm thm);
   5.444      val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (vars_of thm);
   5.445    in instantiate' [] frees thm end;
   5.446  
   5.447 @@ -1083,14 +1080,14 @@
   5.448    (case tvars_of thm of
   5.449      [] => thm
   5.450    | tvars =>
   5.451 -      let val cert = Thm.ctyp_of (Thm.sign_of_thm thm)
   5.452 +      let val cert = Thm.ctyp_of (Thm.theory_of_thm thm)
   5.453        in instantiate' (map (fn ((x, _), S) => SOME (cert (TFree (x, S)))) tvars) [] thm end);
   5.454  
   5.455  fun freeze_all_Vars thm =
   5.456    (case vars_of thm of
   5.457      [] => thm
   5.458    | vars =>
   5.459 -      let val cert = Thm.cterm_of (Thm.sign_of_thm thm)
   5.460 +      let val cert = Thm.cterm_of (Thm.theory_of_thm thm)
   5.461        in instantiate' [] (map (fn ((x, _), T) => SOME (cert (Free (x, T)))) vars) thm end);
   5.462  
   5.463  val freeze_all = freeze_all_Vars o freeze_all_TVars;
     6.1 --- a/src/Pure/tactic.ML	Fri Jun 17 18:33:05 2005 +0200
     6.2 +++ b/src/Pure/tactic.ML	Fri Jun 17 18:33:08 2005 +0200
     6.3 @@ -111,15 +111,15 @@
     6.4    val simplify: bool -> thm list -> thm -> thm
     6.5    val conjunction_tac: tactic
     6.6    val smart_conjunction_tac: int -> tactic
     6.7 -  val prove_multi_plain: Sign.sg -> string list -> term list -> term list ->
     6.8 +  val prove_multi_plain: theory -> string list -> term list -> term list ->
     6.9      (thm list -> tactic) -> thm list
    6.10 -  val prove_multi: Sign.sg -> string list -> term list -> term list ->
    6.11 +  val prove_multi: theory -> string list -> term list -> term list ->
    6.12      (thm list -> tactic) -> thm list
    6.13 -  val prove_multi_standard: Sign.sg -> string list -> term list -> term list ->
    6.14 +  val prove_multi_standard: theory -> string list -> term list -> term list ->
    6.15      (thm list -> tactic) -> thm list
    6.16 -  val prove_plain: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    6.17 -  val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    6.18 -  val prove_standard: Sign.sg -> string list -> term list -> term ->
    6.19 +  val prove_plain: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    6.20 +  val prove: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    6.21 +  val prove_standard: theory -> string list -> term list -> term ->
    6.22      (thm list -> tactic) -> thm
    6.23    val compose_inst_tac' : (indexname * string) list -> (bool * thm * int) ->
    6.24                            int -> tactic
    6.25 @@ -237,16 +237,16 @@
    6.26    let val (_, _, Bi, _) = dest_state(st,i)
    6.27        val params = Logic.strip_params Bi
    6.28    in rev(rename_wrt_term Bi params) end;
    6.29 -  
    6.30 +
    6.31  (*read instantiations with respect to subgoal i of proof state st*)
    6.32  fun read_insts_in_state (st, i, sinsts, rule) =
    6.33 -	let val {sign,...} = rep_thm st
    6.34 -	    and params = params_of_state st i
    6.35 -	    and rts = types_sorts rule and (types,sorts) = types_sorts st
    6.36 -	    fun types'(a,~1) = (case assoc(params,a) of NONE => types(a,~1) | sm => sm)
    6.37 -	      | types'(ixn) = types ixn;
    6.38 -	    val used = Drule.add_used rule (Drule.add_used st []);
    6.39 -	in read_insts sign rts (types',sorts) used sinsts end;
    6.40 +  let val thy = Thm.theory_of_thm st
    6.41 +      and params = params_of_state st i
    6.42 +      and rts = types_sorts rule and (types,sorts) = types_sorts st
    6.43 +      fun types'(a, ~1) = (case assoc_string (params, a) of NONE => types (a, ~1) | sm => sm)
    6.44 +        | types' ixn = types ixn;
    6.45 +      val used = Drule.add_used rule (Drule.add_used st []);
    6.46 +  in read_insts thy rts (types',sorts) used sinsts end;
    6.47  
    6.48  (*Lift and instantiate a rule wrt the given state and subgoal number *)
    6.49  fun lift_inst_rule' (st, i, sinsts, rule) =
    6.50 @@ -285,15 +285,15 @@
    6.51      i.e. Tinsts is not applied to insts.
    6.52  *)
    6.53  fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
    6.54 -let val {maxidx,sign,...} = rep_thm st
    6.55 +let val {maxidx,thy,...} = rep_thm st
    6.56      val paramTs = map #2 (params_of_state st i)
    6.57      and inc = maxidx+1
    6.58      fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> incr_tvar inc T)
    6.59      (*lift only Var, not term, which must be lifted already*)
    6.60 -    fun liftpair (v,t) = (cterm_of sign (liftvar v), cterm_of sign t)
    6.61 +    fun liftpair (v,t) = (cterm_of thy (liftvar v), cterm_of thy t)
    6.62      fun liftTpair (((a, i), S), T) =
    6.63 -      (ctyp_of sign (TVar ((a, i + inc), S)),
    6.64 -       ctyp_of sign (incr_tvar inc T))
    6.65 +      (ctyp_of thy (TVar ((a, i + inc), S)),
    6.66 +       ctyp_of thy (incr_tvar inc T))
    6.67  in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
    6.68                       (lift_rule (st,i) rule)
    6.69  end;
    6.70 @@ -338,7 +338,7 @@
    6.71    increment revcut_rl instead.*)
    6.72  fun make_elim_preserve rl =
    6.73    let val {maxidx,...} = rep_thm rl
    6.74 -      fun cvar ixn = cterm_of (Theory.sign_of ProtoPure.thy) (Var(ixn,propT));
    6.75 +      fun cvar ixn = cterm_of ProtoPure.thy (Var(ixn,propT));
    6.76        val revcut_rl' =
    6.77            instantiate ([],  [(cvar("V",0), cvar("V",maxidx+1)),
    6.78                               (cvar("W",0), cvar("W",maxidx+1))]) revcut_rl
    6.79 @@ -596,11 +596,11 @@
    6.80  fun rename_params_tac xs i =
    6.81    case Library.find_first (not o Syntax.is_identifier) xs of
    6.82        SOME x => error ("Not an identifier: " ^ x)
    6.83 -    | NONE => 
    6.84 +    | NONE =>
    6.85         (if !Logic.auto_rename
    6.86 -	 then (warning "Resetting Logic.auto_rename";
    6.87 -	     Logic.auto_rename := false)
    6.88 -	else (); PRIMITIVE (rename_params_rule (xs, i)));
    6.89 +         then (warning "Resetting Logic.auto_rename";
    6.90 +             Logic.auto_rename := false)
    6.91 +        else (); PRIMITIVE (rename_params_rule (xs, i)));
    6.92  
    6.93  fun rename_tac str i =
    6.94    let val cs = Symbol.explode str in
    6.95 @@ -652,7 +652,7 @@
    6.96      (fn st =>
    6.97        compose_tac (false, Drule.incr_indexes_wrt [] [] [] [st] Drule.conj_intr_thm, 2) i st)
    6.98    | _ => no_tac);
    6.99 -  
   6.100 +
   6.101  val conjunction_tac = ALLGOALS (REPEAT_ALL_NEW conj_tac);
   6.102  
   6.103  fun smart_conjunction_tac 0 = assume_tac 1
   6.104 @@ -662,7 +662,7 @@
   6.105  
   6.106  (** minimal goal interface for programmed proofs *)
   6.107  
   6.108 -fun gen_prove_multi finish_thm sign xs asms props tac =
   6.109 +fun gen_prove_multi finish_thm thy xs asms props tac =
   6.110    let
   6.111      val prop = Logic.mk_conjunction_list props;
   6.112      val statement = Logic.list_implies (asms, prop);
   6.113 @@ -673,9 +673,9 @@
   6.114  
   6.115      fun err msg = raise ERROR_MESSAGE
   6.116        (msg ^ "\nThe error(s) above occurred for the goal statement:\n" ^
   6.117 -        Sign.string_of_term sign (Term.list_all_free (params, statement)));
   6.118 +        Sign.string_of_term thy (Term.list_all_free (params, statement)));
   6.119  
   6.120 -    fun cert_safe t = Thm.cterm_of sign (Envir.beta_norm t)
   6.121 +    fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm t)
   6.122        handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
   6.123  
   6.124      val _ = cert_safe statement;
   6.125 @@ -696,8 +696,8 @@
   6.126  
   6.127      val raw_result = goal' RS Drule.rev_triv_goal;
   6.128      val prop' = prop_of raw_result;
   6.129 -    val _ = conditional (not (Pattern.matches (Sign.tsig_of sign) (prop, prop'))) (fn () =>
   6.130 -      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop'));
   6.131 +    val _ = conditional (not (Pattern.matches (Sign.tsig_of thy) (prop, prop'))) (fn () =>
   6.132 +      err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   6.133    in
   6.134      Drule.conj_elim_precise (length props) raw_result
   6.135      |> map (fn res => res
   6.136 @@ -706,18 +706,18 @@
   6.137        |> finish_thm fixed_tfrees)
   6.138    end;
   6.139  
   6.140 -fun prove_multi_plain sign xs asms prop tac =
   6.141 -  gen_prove_multi (K norm_hhf_plain) sign xs asms prop tac;
   6.142 -fun prove_multi sign xs asms prop tac =
   6.143 +fun prove_multi_plain thy xs asms prop tac =
   6.144 +  gen_prove_multi (K norm_hhf_plain) thy xs asms prop tac;
   6.145 +fun prove_multi thy xs asms prop tac =
   6.146    gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
   6.147        (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
   6.148 -    sign xs asms prop tac;
   6.149 -fun prove_multi_standard sign xs asms prop tac =
   6.150 -  map Drule.standard (prove_multi sign xs asms prop tac);
   6.151 +    thy xs asms prop tac;
   6.152 +fun prove_multi_standard thy xs asms prop tac =
   6.153 +  map Drule.standard (prove_multi thy xs asms prop tac);
   6.154  
   6.155 -fun prove_plain sign xs asms prop tac = hd (prove_multi_plain sign xs asms [prop] tac);
   6.156 -fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac);
   6.157 -fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac);
   6.158 +fun prove_plain thy xs asms prop tac = hd (prove_multi_plain thy xs asms [prop] tac);
   6.159 +fun prove thy xs asms prop tac = hd (prove_multi thy xs asms [prop] tac);
   6.160 +fun prove_standard thy xs asms prop tac = Drule.standard (prove thy xs asms prop tac);
   6.161  
   6.162  end;
   6.163  
     7.1 --- a/src/Pure/thm.ML	Fri Jun 17 18:33:05 2005 +0200
     7.2 +++ b/src/Pure/thm.ML	Fri Jun 17 18:33:08 2005 +0200
     7.3 @@ -3,137 +3,143 @@
     7.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.5      Copyright   1994  University of Cambridge
     7.6  
     7.7 -The core of Isabelle's Meta Logic: certified types and terms, meta
     7.8 -theorems, meta rules (including lifting and resolution).
     7.9 +The very core of Isabelle's Meta Logic: certified types and terms,
    7.10 +meta theorems, meta rules (including lifting and resolution).
    7.11  *)
    7.12  
    7.13  signature BASIC_THM =
    7.14    sig
    7.15    (*certified types*)
    7.16    type ctyp
    7.17 -  val rep_ctyp          : ctyp -> {sign: Sign.sg, T: typ}
    7.18 -  val typ_of            : ctyp -> typ
    7.19 -  val ctyp_of           : Sign.sg -> typ -> ctyp
    7.20 -  val read_ctyp         : Sign.sg -> string -> ctyp
    7.21 +  val rep_ctyp: ctyp -> {thy: theory, sign: theory, T: typ}
    7.22 +  val theory_of_ctyp: ctyp -> theory
    7.23 +  val typ_of: ctyp -> typ
    7.24 +  val ctyp_of: theory -> typ -> ctyp
    7.25 +  val read_ctyp: theory -> string -> ctyp
    7.26  
    7.27    (*certified terms*)
    7.28    type cterm
    7.29    exception CTERM of string
    7.30 -  val rep_cterm         : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int}
    7.31 -  val crep_cterm        : cterm -> {sign: Sign.sg, t: term, T: ctyp, maxidx: int}
    7.32 -  val sign_of_cterm	: cterm -> Sign.sg
    7.33 -  val term_of           : cterm -> term
    7.34 -  val cterm_of          : Sign.sg -> term -> cterm
    7.35 -  val ctyp_of_term      : cterm -> ctyp
    7.36 -  val read_cterm        : Sign.sg -> string * typ -> cterm
    7.37 -  val adjust_maxidx     : cterm -> cterm
    7.38 -  val read_def_cterm    :
    7.39 -    Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    7.40 +  val rep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: typ, maxidx: int}
    7.41 +  val crep_cterm: cterm -> {thy: theory, sign: theory, t: term, T: ctyp, maxidx: int}
    7.42 +  val theory_of_cterm: cterm -> theory
    7.43 +  val sign_of_cterm: cterm -> theory    (*obsolete*)
    7.44 +  val term_of: cterm -> term
    7.45 +  val cterm_of: theory -> term -> cterm
    7.46 +  val ctyp_of_term: cterm -> ctyp
    7.47 +  val read_cterm: theory -> string * typ -> cterm
    7.48 +  val adjust_maxidx: cterm -> cterm
    7.49 +  val read_def_cterm:
    7.50 +    theory * (indexname -> typ option) * (indexname -> sort option) ->
    7.51      string list -> bool -> string * typ -> cterm * (indexname * typ) list
    7.52 -  val read_def_cterms   :
    7.53 -    Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
    7.54 +  val read_def_cterms:
    7.55 +    theory * (indexname -> typ option) * (indexname -> sort option) ->
    7.56      string list -> bool -> (string * typ)list
    7.57      -> cterm list * (indexname * typ)list
    7.58  
    7.59 -  type tag		(* = string * string list *)
    7.60 +  type tag              (* = string * string list *)
    7.61  
    7.62    (*meta theorems*)
    7.63    type thm
    7.64 -  val rep_thm           : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int,
    7.65 -                                  shyps: sort list, hyps: term list, 
    7.66 -                                  tpairs: (term * term) list, prop: term}
    7.67 -  val crep_thm          : thm -> {sign: Sign.sg, der: bool * Proofterm.proof, maxidx: int,
    7.68 -                                  shyps: sort list, hyps: cterm list, 
    7.69 -                                  tpairs: (cterm * cterm) list, prop: cterm}
    7.70 +  val rep_thm: thm ->
    7.71 +   {thy: theory, sign: theory,
    7.72 +    der: bool * Proofterm.proof,
    7.73 +    maxidx: int,
    7.74 +    shyps: sort list,
    7.75 +    hyps: term list,
    7.76 +    tpairs: (term * term) list,
    7.77 +    prop: term}
    7.78 +  val crep_thm: thm ->
    7.79 +   {thy: theory, sign: theory,
    7.80 +    der: bool * Proofterm.proof,
    7.81 +    maxidx: int,
    7.82 +    shyps: sort list,
    7.83 +    hyps: cterm list,
    7.84 +    tpairs: (cterm * cterm) list,
    7.85 +    prop: cterm}
    7.86    exception THM of string * int * thm list
    7.87 -  type 'a attribute 	(* = 'a * thm -> 'a * thm *)
    7.88 -  val eq_thm		: thm * thm -> bool
    7.89 -  val eq_thms		: thm list * thm list -> bool
    7.90 -  val sign_of_thm       : thm -> Sign.sg
    7.91 -  val prop_of           : thm -> term
    7.92 -  val proof_of		: thm -> Proofterm.proof
    7.93 -  val transfer_sg	: Sign.sg -> thm -> thm
    7.94 -  val transfer		: theory -> thm -> thm
    7.95 -  val tpairs_of         : thm -> (term * term) list
    7.96 -  val prems_of          : thm -> term list
    7.97 -  val nprems_of         : thm -> int
    7.98 -  val concl_of          : thm -> term
    7.99 -  val cprop_of          : thm -> cterm
   7.100 -  val extra_shyps       : thm -> sort list
   7.101 -  val strip_shyps       : thm -> thm
   7.102 -  val get_axiom_i       : theory -> string -> thm
   7.103 -  val get_axiom         : theory -> xstring -> thm
   7.104 -  val def_name		: string -> string
   7.105 -  val get_def           : theory -> xstring -> thm
   7.106 -  val axioms_of         : theory -> (string * thm) list
   7.107 +  type 'a attribute     (* = 'a * thm -> 'a * thm *)
   7.108 +  val eq_thm: thm * thm -> bool
   7.109 +  val eq_thms: thm list * thm list -> bool
   7.110 +  val theory_of_thm: thm -> theory
   7.111 +  val sign_of_thm: thm -> theory    (*obsolete*)
   7.112 +  val prop_of: thm -> term
   7.113 +  val proof_of: thm -> Proofterm.proof
   7.114 +  val transfer: theory -> thm -> thm
   7.115 +  val tpairs_of: thm -> (term * term) list
   7.116 +  val prems_of: thm -> term list
   7.117 +  val nprems_of: thm -> int
   7.118 +  val concl_of: thm -> term
   7.119 +  val cprop_of: thm -> cterm
   7.120 +  val extra_shyps: thm -> sort list
   7.121 +  val strip_shyps: thm -> thm
   7.122 +  val get_axiom_i: theory -> string -> thm
   7.123 +  val get_axiom: theory -> xstring -> thm
   7.124 +  val def_name: string -> string
   7.125 +  val get_def: theory -> xstring -> thm
   7.126 +  val axioms_of: theory -> (string * thm) list
   7.127  
   7.128    (*meta rules*)
   7.129 -  val assume            : cterm -> thm
   7.130 -  val compress          : thm -> thm
   7.131 -  val implies_intr      : cterm -> thm -> thm
   7.132 -  val implies_elim      : thm -> thm -> thm
   7.133 -  val forall_intr       : cterm -> thm -> thm
   7.134 -  val forall_elim       : cterm -> thm -> thm
   7.135 -  val reflexive         : cterm -> thm
   7.136 -  val symmetric         : thm -> thm
   7.137 -  val transitive        : thm -> thm -> thm
   7.138 -  val beta_conversion   : bool -> cterm -> thm
   7.139 -  val eta_conversion    : cterm -> thm
   7.140 -  val abstract_rule     : string -> cterm -> thm -> thm
   7.141 -  val combination       : thm -> thm -> thm
   7.142 -  val equal_intr        : thm -> thm -> thm
   7.143 -  val equal_elim        : thm -> thm -> thm
   7.144 -  val implies_intr_hyps : thm -> thm
   7.145 -  val flexflex_rule     : thm -> thm Seq.seq
   7.146 -  val instantiate       :
   7.147 -    (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   7.148 -  val trivial           : cterm -> thm
   7.149 -  val class_triv        : Sign.sg -> class -> thm
   7.150 -  val varifyT           : thm -> thm
   7.151 -  val varifyT'          : (string * sort) list -> thm -> thm * ((string * sort) * indexname) list
   7.152 -  val freezeT           : thm -> thm
   7.153 -  val dest_state        : thm * int ->
   7.154 -    (term * term) list * term list * term * term
   7.155 -  val lift_rule         : (thm * int) -> thm -> thm
   7.156 -  val incr_indexes      : int -> thm -> thm
   7.157 -  val assumption        : int -> thm -> thm Seq.seq
   7.158 -  val eq_assumption     : int -> thm -> thm
   7.159 -  val rotate_rule       : int -> int -> thm -> thm
   7.160 -  val permute_prems     : int -> int -> thm -> thm
   7.161 +  val assume: cterm -> thm
   7.162 +  val compress: thm -> thm
   7.163 +  val implies_intr: cterm -> thm -> thm
   7.164 +  val implies_elim: thm -> thm -> thm
   7.165 +  val forall_intr: cterm -> thm -> thm
   7.166 +  val forall_elim: cterm -> thm -> thm
   7.167 +  val reflexive: cterm -> thm
   7.168 +  val symmetric: thm -> thm
   7.169 +  val transitive: thm -> thm -> thm
   7.170 +  val beta_conversion: bool -> cterm -> thm
   7.171 +  val eta_conversion: cterm -> thm
   7.172 +  val abstract_rule: string -> cterm -> thm -> thm
   7.173 +  val combination: thm -> thm -> thm
   7.174 +  val equal_intr: thm -> thm -> thm
   7.175 +  val equal_elim: thm -> thm -> thm
   7.176 +  val implies_intr_hyps: thm -> thm
   7.177 +  val flexflex_rule: thm -> thm Seq.seq
   7.178 +  val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   7.179 +  val trivial: cterm -> thm
   7.180 +  val class_triv: theory -> class -> thm
   7.181 +  val varifyT: thm -> thm
   7.182 +  val varifyT': (string * sort) list -> thm -> thm * ((string * sort) * indexname) list
   7.183 +  val freezeT: thm -> thm
   7.184 +  val dest_state: thm * int -> (term * term) list * term list * term * term
   7.185 +  val lift_rule: (thm * int) -> thm -> thm
   7.186 +  val incr_indexes: int -> thm -> thm
   7.187 +  val assumption: int -> thm -> thm Seq.seq
   7.188 +  val eq_assumption: int -> thm -> thm
   7.189 +  val rotate_rule: int -> int -> thm -> thm
   7.190 +  val permute_prems: int -> int -> thm -> thm
   7.191    val rename_params_rule: string list * int -> thm -> thm
   7.192 -  val bicompose         : bool -> bool * thm * int ->
   7.193 -    int -> thm -> thm Seq.seq
   7.194 -  val biresolution      : bool -> (bool * thm) list ->
   7.195 -    int -> thm -> thm Seq.seq
   7.196 -  val invoke_oracle_i   : theory -> string -> Sign.sg * Object.T -> thm
   7.197 -  val invoke_oracle     : theory -> xstring -> Sign.sg * Object.T -> thm
   7.198 +  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   7.199 +  val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   7.200 +  val invoke_oracle: theory -> xstring -> theory * Object.T -> thm
   7.201 +  val invoke_oracle_i: theory -> string -> theory * Object.T -> thm
   7.202  end;
   7.203  
   7.204  signature THM =
   7.205  sig
   7.206    include BASIC_THM
   7.207 -  val dest_ctyp         : ctyp -> ctyp list
   7.208 -  val dest_comb         : cterm -> cterm * cterm
   7.209 -  val dest_abs          : string option -> cterm -> cterm * cterm
   7.210 -  val capply            : cterm -> cterm -> cterm
   7.211 -  val cabs              : cterm -> cterm -> cterm
   7.212 -  val major_prem_of	: thm -> term
   7.213 -  val no_prems		: thm -> bool
   7.214 -  val no_attributes	: 'a -> 'a * 'b attribute list
   7.215 -  val apply_attributes	: ('a * thm) * 'a attribute list -> ('a * thm)
   7.216 -  val applys_attributes	: ('a * thm list) * 'a attribute list -> ('a * thm list)
   7.217 -  val get_name_tags	: thm -> string * tag list
   7.218 -  val put_name_tags	: string * tag list -> thm -> thm
   7.219 -  val name_of_thm	: thm -> string
   7.220 -  val tags_of_thm	: thm -> tag list
   7.221 -  val name_thm		: string * thm -> thm
   7.222 -  val rename_boundvars  : term -> term -> thm -> thm
   7.223 -  val cterm_match       : cterm * cterm ->
   7.224 -    (ctyp * ctyp) list * (cterm * cterm) list
   7.225 -  val cterm_first_order_match : cterm * cterm ->
   7.226 -    (ctyp * ctyp) list * (cterm * cterm) list
   7.227 -  val cterm_incr_indexes : int -> cterm -> cterm
   7.228 -  val terms_of_tpairs   : (term * term) list -> term list
   7.229 +  val dest_ctyp: ctyp -> ctyp list
   7.230 +  val dest_comb: cterm -> cterm * cterm
   7.231 +  val dest_abs: string option -> cterm -> cterm * cterm
   7.232 +  val capply: cterm -> cterm -> cterm
   7.233 +  val cabs: cterm -> cterm -> cterm
   7.234 +  val major_prem_of: thm -> term
   7.235 +  val no_prems: thm -> bool
   7.236 +  val no_attributes: 'a -> 'a * 'b attribute list
   7.237 +  val apply_attributes: ('a * thm) * 'a attribute list -> ('a * thm)
   7.238 +  val applys_attributes: ('a * thm list) * 'a attribute list -> ('a * thm list)
   7.239 +  val get_name_tags: thm -> string * tag list
   7.240 +  val put_name_tags: string * tag list -> thm -> thm
   7.241 +  val name_of_thm: thm -> string
   7.242 +  val tags_of_thm: thm -> tag list
   7.243 +  val name_thm: string * thm -> thm
   7.244 +  val rename_boundvars: term -> term -> thm -> thm
   7.245 +  val cterm_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   7.246 +  val cterm_first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   7.247 +  val cterm_incr_indexes: int -> cterm -> cterm
   7.248 +  val terms_of_tpairs: (term * term) list -> term list
   7.249  end;
   7.250  
   7.251  structure Thm: THM =
   7.252 @@ -143,111 +149,116 @@
   7.253  
   7.254  (** certified types **)
   7.255  
   7.256 -(*certified typs under a signature*)
   7.257 +datatype ctyp = Ctyp of {thy_ref: theory_ref, T: typ};
   7.258  
   7.259 -datatype ctyp = Ctyp of {sign_ref: Sign.sg_ref, T: typ};
   7.260 +fun rep_ctyp (Ctyp {thy_ref, T}) =
   7.261 +  let val thy = Theory.deref thy_ref
   7.262 +  in {thy = thy, sign = thy, T = T} end;
   7.263  
   7.264 -fun rep_ctyp (Ctyp {sign_ref, T}) = {sign = Sign.deref sign_ref, T = T};
   7.265 +val theory_of_ctyp = #thy o rep_ctyp;
   7.266 +
   7.267  fun typ_of (Ctyp {T, ...}) = T;
   7.268  
   7.269 -fun ctyp_of sign T =
   7.270 -  Ctyp {sign_ref = Sign.self_ref sign, T = Sign.certify_typ sign T};
   7.271 +fun ctyp_of thy T =
   7.272 +  Ctyp {thy_ref = Theory.self_ref thy, T = Sign.certify_typ thy T};
   7.273  
   7.274 -fun read_ctyp sign s =
   7.275 -  Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K NONE) s};
   7.276 +fun read_ctyp thy s =
   7.277 +  Ctyp {thy_ref = Theory.self_ref thy, T = Sign.read_typ (thy, K NONE) s};
   7.278  
   7.279 -fun dest_ctyp (Ctyp {sign_ref, T = Type (s, Ts)}) =
   7.280 -      map (fn T => Ctyp {sign_ref = sign_ref, T = T}) Ts
   7.281 +fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts)}) =
   7.282 +      map (fn T => Ctyp {thy_ref = thy_ref, T = T}) Ts
   7.283    | dest_ctyp ct = [ct];
   7.284  
   7.285  
   7.286  
   7.287  (** certified terms **)
   7.288  
   7.289 -(*certified terms under a signature, with checked typ and maxidx of Vars*)
   7.290 +(*certified terms with checked typ and maxidx of Vars/TVars*)
   7.291 +
   7.292 +datatype cterm = Cterm of {thy_ref: theory_ref, t: term, T: typ, maxidx: int};
   7.293  
   7.294 -datatype cterm = Cterm of {sign_ref: Sign.sg_ref, t: term, T: typ, maxidx: int};
   7.295 +fun rep_cterm (Cterm {thy_ref, t, T, maxidx}) =
   7.296 +  let val thy =  Theory.deref thy_ref
   7.297 +  in {thy = thy, sign = thy, t = t, T = T, maxidx = maxidx} end;
   7.298  
   7.299 -fun rep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   7.300 -  {sign = Sign.deref sign_ref, t = t, T = T, maxidx = maxidx};
   7.301 +fun crep_cterm (Cterm {thy_ref, t, T, maxidx}) =
   7.302 +  let val thy = Theory.deref thy_ref in
   7.303 +    {thy = thy, sign = thy, t = t, T = Ctyp {thy_ref = thy_ref, T = T}, maxidx = maxidx}
   7.304 +  end;
   7.305  
   7.306 -fun crep_cterm (Cterm {sign_ref, t, T, maxidx}) =
   7.307 -  {sign = Sign.deref sign_ref, t = t, T = Ctyp {sign_ref = sign_ref, T = T},
   7.308 -    maxidx = maxidx};
   7.309 -
   7.310 -fun sign_of_cterm (Cterm {sign_ref, ...}) = Sign.deref sign_ref;
   7.311 +fun theory_of_cterm (Cterm {thy_ref, ...}) = Theory.deref thy_ref;
   7.312 +val sign_of_cterm = theory_of_cterm;
   7.313  
   7.314  fun term_of (Cterm {t, ...}) = t;
   7.315  
   7.316 -fun ctyp_of_term (Cterm {sign_ref, T, ...}) = Ctyp {sign_ref = sign_ref, T = T};
   7.317 +fun ctyp_of_term (Cterm {thy_ref, T, ...}) = Ctyp {thy_ref = thy_ref, T = T};
   7.318  
   7.319 -(*create a cterm by checking a "raw" term with respect to a signature*)
   7.320 -fun cterm_of sign tm =
   7.321 -  let val (t, T, maxidx) = Sign.certify_term (Sign.pp sign) sign tm
   7.322 -  in  Cterm {sign_ref = Sign.self_ref sign, t = t, T = T, maxidx = maxidx}
   7.323 +fun cterm_of thy tm =
   7.324 +  let val (t, T, maxidx) = Sign.certify_term (Sign.pp thy) thy tm
   7.325 +  in  Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx}
   7.326    end;
   7.327  
   7.328  
   7.329  exception CTERM of string;
   7.330  
   7.331  (*Destruct application in cterms*)
   7.332 -fun dest_comb (Cterm {sign_ref, T, maxidx, t = A $ B}) =
   7.333 +fun dest_comb (Cterm {thy_ref, T, maxidx, t = A $ B}) =
   7.334        let val typeA = fastype_of A;
   7.335            val typeB =
   7.336              case typeA of Type("fun",[S,T]) => S
   7.337                          | _ => error "Function type expected in dest_comb";
   7.338        in
   7.339 -      (Cterm {sign_ref=sign_ref, maxidx=maxidx, t=A, T=typeA},
   7.340 -       Cterm {sign_ref=sign_ref, maxidx=maxidx, t=B, T=typeB})
   7.341 +      (Cterm {thy_ref=thy_ref, maxidx=maxidx, t=A, T=typeA},
   7.342 +       Cterm {thy_ref=thy_ref, maxidx=maxidx, t=B, T=typeB})
   7.343        end
   7.344    | dest_comb _ = raise CTERM "dest_comb";
   7.345  
   7.346  (*Destruct abstraction in cterms*)
   7.347 -fun dest_abs a (Cterm {sign_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
   7.348 -      let val (y,N) = variant_abs (getOpt (a,x),ty,M)
   7.349 -      in (Cterm {sign_ref = sign_ref, T = ty, maxidx = 0, t = Free(y,ty)},
   7.350 -          Cterm {sign_ref = sign_ref, T = S, maxidx = maxidx, t = N})
   7.351 +fun dest_abs a (Cterm {thy_ref, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) =
   7.352 +      let val (y,N) = variant_abs (if_none a x, ty, M)
   7.353 +      in (Cterm {thy_ref = thy_ref, T = ty, maxidx = 0, t = Free(y,ty)},
   7.354 +          Cterm {thy_ref = thy_ref, T = S, maxidx = maxidx, t = N})
   7.355        end
   7.356    | dest_abs _ _ = raise CTERM "dest_abs";
   7.357  
   7.358  (*Makes maxidx precise: it is often too big*)
   7.359 -fun adjust_maxidx (ct as Cterm {sign_ref, T, t, maxidx, ...}) =
   7.360 -  if maxidx = ~1 then ct 
   7.361 -  else  Cterm {sign_ref = sign_ref, T = T, maxidx = maxidx_of_term t, t = t};
   7.362 +fun adjust_maxidx (ct as Cterm {thy_ref, T, t, maxidx, ...}) =
   7.363 +  if maxidx = ~1 then ct
   7.364 +  else  Cterm {thy_ref = thy_ref, T = T, maxidx = maxidx_of_term t, t = t};
   7.365  
   7.366  (*Form cterm out of a function and an argument*)
   7.367 -fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
   7.368 -           (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
   7.369 +fun capply (Cterm {t=f, thy_ref=thy_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
   7.370 +           (Cterm {t=x, thy_ref=thy_ref2, T, maxidx=maxidx2}) =
   7.371        if T = dty then
   7.372          Cterm{t = f $ x,
   7.373 -          sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
   7.374 +          thy_ref=Theory.merge_refs(thy_ref1,thy_ref2), T=rty,
   7.375            maxidx=Int.max(maxidx1, maxidx2)}
   7.376        else raise CTERM "capply: types don't agree"
   7.377    | capply _ _ = raise CTERM "capply: first arg is not a function"
   7.378  
   7.379 -fun cabs (Cterm {t=t1, sign_ref=sign_ref1, T=T1, maxidx=maxidx1})
   7.380 -         (Cterm {t=t2, sign_ref=sign_ref2, T=T2, maxidx=maxidx2}) =
   7.381 -      Cterm {t = lambda t1 t2, sign_ref = Sign.merge_refs (sign_ref1,sign_ref2),
   7.382 +fun cabs (Cterm {t=t1, thy_ref=thy_ref1, T=T1, maxidx=maxidx1})
   7.383 +         (Cterm {t=t2, thy_ref=thy_ref2, T=T2, maxidx=maxidx2}) =
   7.384 +      Cterm {t = lambda t1 t2, thy_ref = Theory.merge_refs (thy_ref1,thy_ref2),
   7.385               T = T1 --> T2, maxidx=Int.max(maxidx1, maxidx2)}
   7.386        handle TERM _ => raise CTERM "cabs: first arg is not a variable";
   7.387  
   7.388  (*Matching of cterms*)
   7.389  fun gen_cterm_match mtch
   7.390 -      (Cterm {sign_ref = sign_ref1, maxidx = maxidx1, t = t1, ...},
   7.391 -       Cterm {sign_ref = sign_ref2, maxidx = maxidx2, t = t2, ...}) =
   7.392 +      (Cterm {thy_ref = thy_ref1, maxidx = maxidx1, t = t1, ...},
   7.393 +       Cterm {thy_ref = thy_ref2, maxidx = maxidx2, t = t2, ...}) =
   7.394    let
   7.395 -    val sign_ref = Sign.merge_refs (sign_ref1, sign_ref2);
   7.396 -    val tsig = Sign.tsig_of (Sign.deref sign_ref);
   7.397 +    val thy_ref = Theory.merge_refs (thy_ref1, thy_ref2);
   7.398 +    val tsig = Sign.tsig_of (Theory.deref thy_ref);
   7.399      val (Tinsts, tinsts) = mtch tsig (t1, t2);
   7.400      val maxidx = Int.max (maxidx1, maxidx2);
   7.401      fun mk_cTinsts (ixn, (S, T)) =
   7.402 -      (Ctyp {sign_ref = sign_ref, T = TVar (ixn, S)},
   7.403 -       Ctyp {sign_ref = sign_ref, T = T});
   7.404 +      (Ctyp {thy_ref = thy_ref, T = TVar (ixn, S)},
   7.405 +       Ctyp {thy_ref = thy_ref, T = T});
   7.406      fun mk_ctinsts (ixn, (T, t)) =
   7.407        let val T = Envir.typ_subst_TVars Tinsts T
   7.408        in
   7.409 -        (Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
   7.410 -         Cterm {sign_ref = sign_ref, maxidx = maxidx, T = T, t = t})
   7.411 +        (Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = Var (ixn, T)},
   7.412 +         Cterm {thy_ref = thy_ref, maxidx = maxidx, T = T, t = t})
   7.413        end;
   7.414    in (map mk_cTinsts (Vartab.dest Tinsts),
   7.415      map mk_ctinsts (Vartab.dest tinsts))
   7.416 @@ -257,10 +268,10 @@
   7.417  val cterm_first_order_match = gen_cterm_match Pattern.first_order_match;
   7.418  
   7.419  (*Incrementing indexes*)
   7.420 -fun cterm_incr_indexes i (ct as Cterm {sign_ref, maxidx, t, T}) =
   7.421 -  if i < 0 then raise CTERM "negative increment" else 
   7.422 +fun cterm_incr_indexes i (ct as Cterm {thy_ref, maxidx, t, T}) =
   7.423 +  if i < 0 then raise CTERM "negative increment" else
   7.424    if i = 0 then ct else
   7.425 -    Cterm {sign_ref = sign_ref, maxidx = maxidx + i,
   7.426 +    Cterm {thy_ref = thy_ref, maxidx = maxidx + i,
   7.427        t = Logic.incr_indexes ([], i) t, T = Term.incr_tvar i T};
   7.428  
   7.429  
   7.430 @@ -268,10 +279,10 @@
   7.431  (** read cterms **)   (*exception ERROR*)
   7.432  
   7.433  (*read terms, infer types, certify terms*)
   7.434 -fun read_def_cterms (sign, types, sorts) used freeze sTs =
   7.435 +fun read_def_cterms (thy, types, sorts) used freeze sTs =
   7.436    let
   7.437 -    val (ts', tye) = Sign.read_def_terms (sign, types, sorts) used freeze sTs;
   7.438 -    val cts = map (cterm_of sign) ts'
   7.439 +    val (ts', tye) = Sign.read_def_terms (thy, types, sorts) used freeze sTs;
   7.440 +    val cts = map (cterm_of thy) ts'
   7.441        handle TYPE (msg, _, _) => error msg
   7.442             | TERM (msg, _) => error msg;
   7.443    in (cts, tye) end;
   7.444 @@ -281,7 +292,7 @@
   7.445    let val ([ct],tye) = read_def_cterms args used freeze [aT]
   7.446    in (ct,tye) end;
   7.447  
   7.448 -fun read_cterm sign = #1 o read_def_cterm (sign, K NONE, K NONE) [] true;
   7.449 +fun read_cterm thy = #1 o read_def_cterm (thy, K NONE, K NONE) [] true;
   7.450  
   7.451  
   7.452  (*tags provide additional comment, apart from the axiom/theorem name*)
   7.453 @@ -293,7 +304,7 @@
   7.454  structure Pt = Proofterm;
   7.455  
   7.456  datatype thm = Thm of
   7.457 - {sign_ref: Sign.sg_ref,       (*mutable reference to signature*)
   7.458 + {thy_ref: theory_ref,         (*dynamic reference to theory*)
   7.459    der: bool * Pt.proof,        (*derivation*)
   7.460    maxidx: int,                 (*maximum index of any Var or TVar*)
   7.461    shyps: sort list,            (*sort hypotheses*)
   7.462 @@ -306,23 +317,28 @@
   7.463  fun attach_tpairs tpairs prop =
   7.464    Logic.list_implies (map Logic.mk_equals tpairs, prop);
   7.465  
   7.466 -fun rep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   7.467 -  {sign = Sign.deref sign_ref, der = der, maxidx = maxidx,
   7.468 -    shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
   7.469 +fun rep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   7.470 +  let val thy = Theory.deref thy_ref in
   7.471 +   {thy = thy, sign = thy, der = der, maxidx = maxidx,
   7.472 +    shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
   7.473 +  end;
   7.474  
   7.475 -(*Version of rep_thm returning cterms instead of terms*)
   7.476 -fun crep_thm (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   7.477 -  let fun ctermf max t = Cterm{sign_ref=sign_ref, t=t, T=propT, maxidx=max};
   7.478 -  in {sign = Sign.deref sign_ref, der = der, maxidx = maxidx, shyps = shyps,
   7.479 -      hyps = map (ctermf ~1) hyps,
   7.480 -      tpairs = map (pairself (ctermf maxidx)) tpairs,
   7.481 -      prop = ctermf maxidx prop}
   7.482 +(*version of rep_thm returning cterms instead of terms*)
   7.483 +fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   7.484 +  let
   7.485 +    val thy = Theory.deref thy_ref;
   7.486 +    fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max};
   7.487 +  in
   7.488 +   {thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps,
   7.489 +    hyps = map (cterm ~1) hyps,
   7.490 +    tpairs = map (pairself (cterm maxidx)) tpairs,
   7.491 +    prop = cterm maxidx prop}
   7.492    end;
   7.493  
   7.494  (*errors involving theorems*)
   7.495  exception THM of string * int * thm list;
   7.496  
   7.497 -(*attributes subsume any kind of rules or addXXXs modifiers*)
   7.498 +(*attributes subsume any kind of rules or context modifiers*)
   7.499  type 'a attribute = 'a * thm -> 'a * thm;
   7.500  
   7.501  fun no_attributes x = (x, []);
   7.502 @@ -331,12 +347,12 @@
   7.503  
   7.504  fun eq_thm (th1, th2) =
   7.505    let
   7.506 -    val {sign = sg1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} =
   7.507 +    val {thy = thy1, shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} =
   7.508        rep_thm th1;
   7.509 -    val {sign = sg2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} =
   7.510 +    val {thy = thy2, shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} =
   7.511        rep_thm th2;
   7.512    in
   7.513 -    Sign.joinable (sg1, sg2) andalso
   7.514 +    (subthy (thy1, thy2) orelse subthy (thy2, thy1)) andalso
   7.515      Sorts.eq_set_sort (shyps1, shyps2) andalso
   7.516      aconvs (hyps1, hyps2) andalso
   7.517      aconvs (terms_of_tpairs tpairs1, terms_of_tpairs tpairs2) andalso
   7.518 @@ -345,30 +361,30 @@
   7.519  
   7.520  val eq_thms = Library.equal_lists eq_thm;
   7.521  
   7.522 -fun sign_of_thm (Thm {sign_ref, ...}) = Sign.deref sign_ref;
   7.523 +fun theory_of_thm (Thm {thy_ref, ...}) = Theory.deref thy_ref;
   7.524 +val sign_of_thm = theory_of_thm;
   7.525 +
   7.526  fun prop_of (Thm {prop, ...}) = prop;
   7.527  fun proof_of (Thm {der = (_, proof), ...}) = proof;
   7.528  
   7.529 -(*merge signatures of two theorems; raise exception if incompatible*)
   7.530 -fun merge_thm_sgs
   7.531 -    (th1 as Thm {sign_ref = sgr1, ...}, th2 as Thm {sign_ref = sgr2, ...}) =
   7.532 -  Sign.merge_refs (sgr1, sgr2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   7.533 +(*merge theories of two theorems; raise exception if incompatible*)
   7.534 +fun merge_thm_thys
   7.535 +    (th1 as Thm {thy_ref = r1, ...}, th2 as Thm {thy_ref = r2, ...}) =
   7.536 +  Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
   7.537  
   7.538  (*transfer thm to super theory (non-destructive)*)
   7.539 -fun transfer_sg sign' thm =
   7.540 +fun transfer thy' thm =
   7.541    let
   7.542 -    val Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm;
   7.543 -    val sign = Sign.deref sign_ref;
   7.544 +    val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm;
   7.545 +    val thy = Theory.deref thy_ref;
   7.546    in
   7.547 -    if Sign.eq_sg (sign, sign') then thm
   7.548 -    else if Sign.subsig (sign, sign') then
   7.549 -      Thm {sign_ref = Sign.self_ref sign', der = der, maxidx = maxidx,
   7.550 +    if eq_thy (thy, thy') then thm
   7.551 +    else if subthy (thy, thy') then
   7.552 +      Thm {thy_ref = Theory.self_ref thy', der = der, maxidx = maxidx,
   7.553          shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
   7.554      else raise THM ("transfer: not a super theory", 0, [thm])
   7.555    end;
   7.556  
   7.557 -val transfer = transfer_sg o Theory.sign_of;
   7.558 -
   7.559  (*maps object-rule to tpairs*)
   7.560  fun tpairs_of (Thm {tpairs, ...}) = tpairs;
   7.561  
   7.562 @@ -391,8 +407,8 @@
   7.563  fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop;
   7.564  
   7.565  (*the statement of any thm is a cterm*)
   7.566 -fun cprop_of (Thm {sign_ref, maxidx, prop, ...}) =
   7.567 -  Cterm {sign_ref = sign_ref, maxidx = maxidx, T = propT, t = prop};
   7.568 +fun cprop_of (Thm {thy_ref, maxidx, prop, ...}) =
   7.569 +  Cterm {thy_ref = thy_ref, maxidx = maxidx, T = propT, t = prop};
   7.570  
   7.571  
   7.572  
   7.573 @@ -443,16 +459,16 @@
   7.574  
   7.575  (* fix_shyps *)
   7.576  
   7.577 -fun all_sorts_nonempty sign_ref = isSome (Sign.universal_witness (Sign.deref sign_ref));
   7.578 +val all_sorts_nonempty = is_some o Sign.universal_witness o Theory.deref;
   7.579  
   7.580  (*preserve sort contexts of rule premises and substituted types*)
   7.581 -fun fix_shyps thms Ts (thm as Thm {sign_ref, der, maxidx, hyps, tpairs, prop, ...}) =
   7.582 +fun fix_shyps thms Ts (thm as Thm {thy_ref, der, maxidx, hyps, tpairs, prop, ...}) =
   7.583    Thm
   7.584 -   {sign_ref = sign_ref,
   7.585 +   {thy_ref = thy_ref,
   7.586      der = der,             (*no new derivation, as other rules call this*)
   7.587      maxidx = maxidx,
   7.588      shyps =
   7.589 -      if all_sorts_nonempty sign_ref then []
   7.590 +      if all_sorts_nonempty thy_ref then []
   7.591        else add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))),
   7.592      hyps = hyps, tpairs = tpairs, prop = prop}
   7.593  
   7.594 @@ -461,15 +477,14 @@
   7.595  
   7.596  (*remove extra sorts that are non-empty by virtue of type signature information*)
   7.597  fun strip_shyps (thm as Thm {shyps = [], ...}) = thm
   7.598 -  | strip_shyps (thm as Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   7.599 +  | strip_shyps (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   7.600        let
   7.601 -        val sign = Sign.deref sign_ref;
   7.602 -
   7.603 +        val thy = Theory.deref thy_ref;
   7.604          val present_sorts = add_thm_sorts (thm, []);
   7.605          val extra_shyps = Sorts.rems_sort (shyps, present_sorts);
   7.606 -        val witnessed_shyps = Sign.witness_sorts sign present_sorts extra_shyps;
   7.607 +        val witnessed_shyps = Sign.witness_sorts thy present_sorts extra_shyps;
   7.608        in
   7.609 -        Thm {sign_ref = sign_ref, der = der, maxidx = maxidx,
   7.610 +        Thm {thy_ref = thy_ref, der = der, maxidx = maxidx,
   7.611               shyps = Sorts.rems_sort (shyps, map #2 witnessed_shyps),
   7.612               hyps = hyps, tpairs = tpairs, prop = prop}
   7.613        end;
   7.614 @@ -478,33 +493,28 @@
   7.615  
   7.616  (** Axioms **)
   7.617  
   7.618 -(*look up the named axiom in the theory*)
   7.619 +(*look up the named axiom in the theory or its ancestors*)
   7.620  fun get_axiom_i theory name =
   7.621    let
   7.622 -    fun get_ax [] = NONE
   7.623 -      | get_ax (thy :: thys) =
   7.624 -          let val {sign, axioms = (_, axioms), ...} = Theory.rep_theory thy in
   7.625 -            (case Symtab.lookup (axioms, name) of
   7.626 -              SOME t =>
   7.627 -                SOME (fix_shyps [] []
   7.628 -                  (Thm {sign_ref = Sign.self_ref sign,
   7.629 -                    der = Pt.infer_derivs' I
   7.630 -                      (false, Pt.axm_proof name t),
   7.631 -                    maxidx = maxidx_of_term t,
   7.632 -                    shyps = [], 
   7.633 -                    hyps = [], 
   7.634 -                    tpairs = [],
   7.635 -                    prop = t}))
   7.636 -            | NONE => get_ax thys)
   7.637 -          end;
   7.638 +    fun get_ax thy =
   7.639 +      Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name)
   7.640 +      |> Option.map (fn t =>
   7.641 +          fix_shyps [] []
   7.642 +            (Thm {thy_ref = Theory.self_ref thy,
   7.643 +              der = Pt.infer_derivs' I (false, Pt.axm_proof name t),
   7.644 +              maxidx = maxidx_of_term t,
   7.645 +              shyps = [],
   7.646 +              hyps = [],
   7.647 +              tpairs = [],
   7.648 +              prop = t}));
   7.649    in
   7.650 -    (case get_ax (theory :: Theory.ancestors_of theory) of
   7.651 +    (case get_first get_ax (theory :: Theory.ancestors_of theory) of
   7.652        SOME thm => thm
   7.653      | NONE => raise THEORY ("No axiom " ^ quote name, [theory]))
   7.654    end;
   7.655  
   7.656  fun get_axiom thy =
   7.657 -  get_axiom_i thy o NameSpace.intern (#1 (#axioms (Theory.rep_theory thy)));
   7.658 +  get_axiom_i thy o NameSpace.intern (Theory.axiom_space thy);
   7.659  
   7.660  fun def_name name = name ^ "_def";
   7.661  fun get_def thy = get_axiom thy o def_name;
   7.662 @@ -521,9 +531,9 @@
   7.663  fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) =
   7.664    Pt.get_name_tags hyps prop prf;
   7.665  
   7.666 -fun put_name_tags x (Thm {sign_ref, der = (ora, prf), maxidx,
   7.667 -      shyps, hyps, tpairs = [], prop}) = Thm {sign_ref = sign_ref,
   7.668 -        der = (ora, Pt.thm_proof (Sign.deref sign_ref) x hyps prop prf),
   7.669 +fun put_name_tags x (Thm {thy_ref, der = (ora, prf), maxidx,
   7.670 +      shyps, hyps, tpairs = [], prop}) = Thm {thy_ref = thy_ref,
   7.671 +        der = (ora, Pt.thm_proof (Theory.deref thy_ref) x hyps prop prf),
   7.672          maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop}
   7.673    | put_name_tags _ thm =
   7.674        raise THM ("put_name_tags: unsolved flex-flex constraints", 0, [thm]);
   7.675 @@ -536,12 +546,12 @@
   7.676  
   7.677  (*Compression of theorems -- a separate rule, not integrated with the others,
   7.678    as it could be slow.*)
   7.679 -fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) = 
   7.680 -    Thm {sign_ref = sign_ref, 
   7.681 +fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
   7.682 +    Thm {thy_ref = thy_ref,
   7.683           der = der,     (*No derivation recorded!*)
   7.684           maxidx = maxidx,
   7.685 -         shyps = shyps, 
   7.686 -         hyps = map Term.compress_term hyps, 
   7.687 +         shyps = shyps,
   7.688 +         hyps = map Term.compress_term hyps,
   7.689           tpairs = map (pairself Term.compress_term) tpairs,
   7.690           prop = Term.compress_term prop};
   7.691  
   7.692 @@ -556,17 +566,17 @@
   7.693  
   7.694  (*The assumption rule A|-A in a theory*)
   7.695  fun assume raw_ct : thm =
   7.696 -  let val ct as Cterm {sign_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
   7.697 +  let val ct as Cterm {thy_ref, t=prop, T, maxidx} = adjust_maxidx raw_ct
   7.698    in  if T<>propT then
   7.699          raise THM("assume: assumptions must have type prop", 0, [])
   7.700        else if maxidx <> ~1 then
   7.701          raise THM("assume: assumptions may not contain scheme variables",
   7.702                    maxidx, [])
   7.703 -      else Thm{sign_ref   = sign_ref,
   7.704 +      else Thm{thy_ref   = thy_ref,
   7.705                 der    = Pt.infer_derivs' I (false, Pt.Hyp prop),
   7.706 -               maxidx = ~1, 
   7.707 -               shyps  = add_term_sorts(prop,[]), 
   7.708 -               hyps   = [prop], 
   7.709 +               maxidx = ~1,
   7.710 +               shyps  = add_term_sorts(prop,[]),
   7.711 +               hyps   = [prop],
   7.712                 tpairs = [],
   7.713                 prop   = prop}
   7.714    end;
   7.715 @@ -578,12 +588,12 @@
   7.716    -------
   7.717    A ==> B
   7.718  *)
   7.719 -fun implies_intr cA (thB as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs,prop}) : thm =
   7.720 -  let val Cterm {sign_ref=sign_refA, t=A, T, maxidx=maxidxA} = cA
   7.721 +fun implies_intr cA (thB as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) : thm =
   7.722 +  let val Cterm {thy_ref=thy_refA, t=A, T, maxidx=maxidxA} = cA
   7.723    in  if T<>propT then
   7.724          raise THM("implies_intr: assumptions must have type prop", 0, [thB])
   7.725        else
   7.726 -         Thm{sign_ref = Sign.merge_refs (sign_ref,sign_refA),  
   7.727 +         Thm{thy_ref = Theory.merge_refs (thy_ref,thy_refA),
   7.728               der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
   7.729               maxidx = Int.max(maxidxA, maxidx),
   7.730               shyps = add_term_sorts (A, shyps),
   7.731 @@ -591,7 +601,7 @@
   7.732               tpairs = tpairs,
   7.733               prop = implies$A$prop}
   7.734        handle TERM _ =>
   7.735 -        raise THM("implies_intr: incompatible signatures", 0, [thB])
   7.736 +        raise THM("implies_intr: incompatible theories", 0, [thB])
   7.737    end;
   7.738  
   7.739  
   7.740 @@ -608,7 +618,7 @@
   7.741              imp$A$B =>
   7.742                  if imp=implies andalso  A aconv propA
   7.743                  then
   7.744 -                  Thm{sign_ref= merge_thm_sgs(thAB,thA),
   7.745 +                  Thm{thy_ref= merge_thm_thys (thAB, thA),
   7.746                        der = Pt.infer_derivs (curry Pt.%%) der derA,
   7.747                        maxidx = Int.max(maxA,maxidx),
   7.748                        shyps = Sorts.union_sort (shypsA, shyps),
   7.749 @@ -624,10 +634,10 @@
   7.750    -----
   7.751    !!x.A
   7.752  *)
   7.753 -fun forall_intr cx (th as Thm{sign_ref,der,maxidx,hyps,tpairs,prop,...}) =
   7.754 +fun forall_intr cx (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) =
   7.755    let val x = term_of cx;
   7.756        fun result a T = fix_shyps [th] []
   7.757 -        (Thm{sign_ref = sign_ref, 
   7.758 +        (Thm{thy_ref = thy_ref,
   7.759               der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
   7.760               maxidx = maxidx,
   7.761               shyps = [],
   7.762 @@ -649,35 +659,35 @@
   7.763    ------
   7.764    A[t/x]
   7.765  *)
   7.766 -fun forall_elim ct (th as Thm{sign_ref,der,maxidx,hyps,tpairs,prop,...}) : thm =
   7.767 -  let val Cterm {sign_ref=sign_reft, t, T, maxidx=maxt} = ct
   7.768 +fun forall_elim ct (th as Thm{thy_ref,der,maxidx,hyps,tpairs,prop,...}) : thm =
   7.769 +  let val Cterm {thy_ref=thy_reft, t, T, maxidx=maxt} = ct
   7.770    in  case prop of
   7.771          Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A =>
   7.772            if T<>qary then
   7.773                raise THM("forall_elim: type mismatch", 0, [th])
   7.774            else fix_shyps [th] []
   7.775 -                    (Thm{sign_ref= Sign.merge_refs(sign_ref,sign_reft),
   7.776 +                    (Thm{thy_ref= Theory.merge_refs(thy_ref,thy_reft),
   7.777                           der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
   7.778                           maxidx = Int.max(maxidx, maxt),
   7.779                           shyps = [],
   7.780 -                         hyps = hyps,  
   7.781 +                         hyps = hyps,
   7.782                           tpairs = tpairs,
   7.783                           prop = betapply(A,t)})
   7.784        | _ => raise THM("forall_elim: not quantified", 0, [th])
   7.785    end
   7.786    handle TERM _ =>
   7.787 -         raise THM("forall_elim: incompatible signatures", 0, [th]);
   7.788 +         raise THM("forall_elim: incompatible theories", 0, [th]);
   7.789  
   7.790  
   7.791  (* Equality *)
   7.792  
   7.793  (*The reflexivity rule: maps  t   to the theorem   t==t   *)
   7.794  fun reflexive ct =
   7.795 -  let val Cterm {sign_ref, t, T, maxidx} = ct
   7.796 -  in Thm{sign_ref= sign_ref, 
   7.797 +  let val Cterm {thy_ref, t, T, maxidx} = ct
   7.798 +  in Thm{thy_ref= thy_ref,
   7.799           der = Pt.infer_derivs' I (false, Pt.reflexive),
   7.800           shyps = add_term_sorts (t, []),
   7.801 -         hyps = [], 
   7.802 +         hyps = [],
   7.803           maxidx = maxidx,
   7.804           tpairs = [],
   7.805           prop = Logic.mk_equals(t,t)}
   7.806 @@ -688,11 +698,11 @@
   7.807    ----
   7.808    u==t
   7.809  *)
   7.810 -fun symmetric (th as Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
   7.811 +fun symmetric (th as Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
   7.812    case prop of
   7.813        (eq as Const("==", Type (_, [T, _]))) $ t $ u =>
   7.814          (*no fix_shyps*)
   7.815 -          Thm{sign_ref = sign_ref,
   7.816 +          Thm{thy_ref = thy_ref,
   7.817                der = Pt.infer_derivs' Pt.symmetric der,
   7.818                maxidx = maxidx,
   7.819                shyps = shyps,
   7.820 @@ -709,14 +719,14 @@
   7.821  fun transitive th1 th2 =
   7.822    let val Thm{der=der1, maxidx=max1, hyps=hyps1, shyps=shyps1, tpairs=tpairs1, prop=prop1,...} = th1
   7.823        and Thm{der=der2, maxidx=max2, hyps=hyps2, shyps=shyps2, tpairs=tpairs2, prop=prop2,...} = th2;
   7.824 -      fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2])
   7.825 +      fun err msg = raise THM("transitive: "^msg, 0, [th1,th2])
   7.826    in case (prop1,prop2) of
   7.827         ((eq as Const("==", Type (_, [T, _]))) $ t1 $ u, Const("==",_) $ u' $ t2) =>
   7.828            if not (u aconv u') then err"middle term"
   7.829            else
   7.830 -                 Thm{sign_ref= merge_thm_sgs(th1,th2), 
   7.831 +                 Thm{thy_ref= merge_thm_thys (th1, th2),
   7.832                       der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
   7.833 -                     maxidx = Int.max(max1,max2), 
   7.834 +                     maxidx = Int.max(max1,max2),
   7.835                       shyps = Sorts.union_sort (shyps1, shyps2),
   7.836                       hyps = union_term(hyps1,hyps2),
   7.837                       tpairs = tpairs1 @ tpairs2,
   7.838 @@ -728,9 +738,9 @@
   7.839    Fully beta-reduces the term if full=true
   7.840  *)
   7.841  fun beta_conversion full ct =
   7.842 -  let val Cterm {sign_ref, t, T, maxidx} = ct
   7.843 +  let val Cterm {thy_ref, t, T, maxidx} = ct
   7.844    in Thm
   7.845 -    {sign_ref = sign_ref,  
   7.846 +    {thy_ref = thy_ref,
   7.847       der = Pt.infer_derivs' I (false, Pt.reflexive),
   7.848       maxidx = maxidx,
   7.849       shyps = add_term_sorts (t, []),
   7.850 @@ -743,9 +753,9 @@
   7.851    end;
   7.852  
   7.853  fun eta_conversion ct =
   7.854 -  let val Cterm {sign_ref, t, T, maxidx} = ct
   7.855 +  let val Cterm {thy_ref, t, T, maxidx} = ct
   7.856    in Thm
   7.857 -    {sign_ref = sign_ref,  
   7.858 +    {thy_ref = thy_ref,
   7.859       der = Pt.infer_derivs' I (false, Pt.reflexive),
   7.860       maxidx = maxidx,
   7.861       shyps = add_term_sorts (t, []),
   7.862 @@ -760,16 +770,16 @@
   7.863    ------------
   7.864    %x.t == %x.u
   7.865  *)
   7.866 -fun abstract_rule a cx (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs,prop}) =
   7.867 +fun abstract_rule a cx (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs,prop}) =
   7.868    let val x = term_of cx;
   7.869        val (t,u) = Logic.dest_equals prop
   7.870              handle TERM _ =>
   7.871                  raise THM("abstract_rule: premise not an equality", 0, [th])
   7.872        fun result T =
   7.873 -           Thm{sign_ref = sign_ref,
   7.874 +           Thm{thy_ref = thy_ref,
   7.875                 der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
   7.876 -               maxidx = maxidx, 
   7.877 -               shyps = add_typ_sorts (T, shyps), 
   7.878 +               maxidx = maxidx,
   7.879 +               shyps = add_typ_sorts (T, shyps),
   7.880                 hyps = hyps,
   7.881                 tpairs = tpairs,
   7.882                 prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)),
   7.883 @@ -790,27 +800,27 @@
   7.884     f(t) == g(u)
   7.885  *)
   7.886  fun combination th1 th2 =
   7.887 -  let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
   7.888 +  let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
   7.889                tpairs=tpairs1, prop=prop1,...} = th1
   7.890 -      and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   7.891 +      and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
   7.892                tpairs=tpairs2, prop=prop2,...} = th2
   7.893        fun chktypes fT tT =
   7.894              (case fT of
   7.895 -                Type("fun",[T1,T2]) => 
   7.896 +                Type("fun",[T1,T2]) =>
   7.897                      if T1 <> tT then
   7.898                           raise THM("combination: types", 0, [th1,th2])
   7.899                      else ()
   7.900 -                | _ => raise THM("combination: not function type", 0, 
   7.901 +                | _ => raise THM("combination: not function type", 0,
   7.902                                   [th1,th2]))
   7.903    in case (prop1,prop2)  of
   7.904         (Const ("==", Type ("fun", [fT, _])) $ f $ g,
   7.905          Const ("==", Type ("fun", [tT, _])) $ t $ u) =>
   7.906            (chktypes fT tT;
   7.907                          (*no fix_shyps*)
   7.908 -                        Thm{sign_ref = merge_thm_sgs(th1,th2), 
   7.909 +                        Thm{thy_ref = merge_thm_thys(th1,th2),
   7.910                              der = Pt.infer_derivs
   7.911                                (Pt.combination f g t u fT) der1 der2,
   7.912 -                            maxidx = Int.max(max1,max2), 
   7.913 +                            maxidx = Int.max(max1,max2),
   7.914                              shyps = Sorts.union_sort(shyps1,shyps2),
   7.915                              hyps = union_term(hyps1,hyps2),
   7.916                              tpairs = tpairs1 @ tpairs2,
   7.917 @@ -825,9 +835,9 @@
   7.918         A == B
   7.919  *)
   7.920  fun equal_intr th1 th2 =
   7.921 -  let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
   7.922 +  let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1,
   7.923                tpairs=tpairs1, prop=prop1,...} = th1
   7.924 -      and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
   7.925 +      and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2,
   7.926                tpairs=tpairs2, prop=prop2,...} = th2;
   7.927        fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2])
   7.928    in case (prop1,prop2) of
   7.929 @@ -835,7 +845,7 @@
   7.930            if A aconv A' andalso B aconv B'
   7.931            then
   7.932              (*no fix_shyps*)
   7.933 -              Thm{sign_ref = merge_thm_sgs(th1,th2),
   7.934 +              Thm{thy_ref = merge_thm_thys(th1,th2),
   7.935                    der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
   7.936                    maxidx = Int.max(max1,max2),
   7.937                    shyps = Sorts.union_sort(shyps1,shyps2),
   7.938 @@ -860,7 +870,7 @@
   7.939         Const("==",_) $ A $ B =>
   7.940            if not (prop2 aconv A) then err"not equal"  else
   7.941              fix_shyps [th1, th2] []
   7.942 -              (Thm{sign_ref= merge_thm_sgs(th1,th2), 
   7.943 +              (Thm{thy_ref= merge_thm_thys(th1,th2),
   7.944                     der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
   7.945                     maxidx = Int.max(max1,max2),
   7.946                     shyps = [],
   7.947 @@ -876,13 +886,13 @@
   7.948  
   7.949  (*Discharge all hypotheses.  Need not verify cterms or call fix_shyps.
   7.950    Repeated hypotheses are discharged only once;  fold cannot do this*)
   7.951 -fun implies_intr_hyps (Thm{sign_ref, der, maxidx, shyps, hyps=A::As, tpairs, prop}) =
   7.952 +fun implies_intr_hyps (Thm{thy_ref, der, maxidx, shyps, hyps=A::As, tpairs, prop}) =
   7.953        implies_intr_hyps (*no fix_shyps*)
   7.954 -            (Thm{sign_ref = sign_ref, 
   7.955 +            (Thm{thy_ref = thy_ref,
   7.956                   der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
   7.957 -                 maxidx = maxidx, 
   7.958 +                 maxidx = maxidx,
   7.959                   shyps = shyps,
   7.960 -                 hyps = disch(As,A),  
   7.961 +                 hyps = disch(As,A),
   7.962                   tpairs = tpairs,
   7.963                   prop = implies$A$prop})
   7.964    | implies_intr_hyps th = th;
   7.965 @@ -891,7 +901,7 @@
   7.966    Instantiates the theorem and deletes trivial tpairs.
   7.967    Resulting sequence may contain multiple elements if the tpairs are
   7.968      not all flex-flex. *)
   7.969 -fun flexflex_rule (th as Thm{sign_ref, der, maxidx, hyps, tpairs, prop, ...}) =
   7.970 +fun flexflex_rule (th as Thm{thy_ref, der, maxidx, hyps, tpairs, prop, ...}) =
   7.971    let fun newthm env =
   7.972            if Envir.is_empty env then th
   7.973            else
   7.974 @@ -900,17 +910,17 @@
   7.975                  (*Remove trivial tpairs, of the form t=t*)
   7.976                val distpairs = List.filter (not o op aconv) ntpairs
   7.977            in  fix_shyps [th] (env_codT env)
   7.978 -                (Thm{sign_ref = sign_ref, 
   7.979 +                (Thm{thy_ref = thy_ref,
   7.980                       der = Pt.infer_derivs' (Pt.norm_proof' env) der,
   7.981                       maxidx = maxidx_of_terms (newprop ::
   7.982                         terms_of_tpairs distpairs),
   7.983 -                     shyps = [], 
   7.984 +                     shyps = [],
   7.985                       hyps = hyps,
   7.986                       tpairs = distpairs,
   7.987                       prop = newprop})
   7.988            end;
   7.989    in Seq.map newthm
   7.990 -            (Unify.smash_unifiers(Sign.deref sign_ref, Envir.empty maxidx, tpairs))
   7.991 +            (Unify.smash_unifiers(Theory.deref thy_ref, Envir.empty maxidx, tpairs))
   7.992    end;
   7.993  
   7.994  (*Instantiation of Vars
   7.995 @@ -924,42 +934,39 @@
   7.996  (*Check that all the terms are Vars and are distinct*)
   7.997  fun instl_ok ts = forall is_Var ts andalso null(findrep ts);
   7.998  
   7.999 -fun prt_typing sg_ref t T =
  7.1000 -  let val sg = Sign.deref sg_ref in
  7.1001 -    Pretty.block [Sign.pretty_term sg t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ sg T]
  7.1002 -  end;
  7.1003 -
  7.1004 -fun prt_type sg_ref T = Sign.pretty_typ (Sign.deref sg_ref) T;
  7.1005 +fun pretty_typing thy t T =
  7.1006 +  Pretty.block [Sign.pretty_term thy t, Pretty.str " ::", Pretty.brk 1, Sign.pretty_typ thy T];
  7.1007  
  7.1008  (*For instantiate: process pair of cterms, merge theories*)
  7.1009 -fun add_ctpair ((ct,cu), (sign_ref,tpairs)) =
  7.1010 +fun add_ctpair ((ct,cu), (thy_ref,tpairs)) =
  7.1011    let
  7.1012 -    val Cterm {sign_ref=sign_reft, t=t, T= T, ...} = ct
  7.1013 -    and Cterm {sign_ref=sign_refu, t=u, T= U, ...} = cu;
  7.1014 -    val sign_ref_merged = Sign.merge_refs (sign_ref, Sign.merge_refs (sign_reft, sign_refu));
  7.1015 +    val Cterm {thy_ref=thy_reft, t=t, T= T, ...} = ct
  7.1016 +    and Cterm {thy_ref=thy_refu, t=u, T= U, ...} = cu;
  7.1017 +    val thy_ref_merged = Theory.merge_refs (thy_ref, Theory.merge_refs (thy_reft, thy_refu));
  7.1018 +    val thy_merged = Theory.deref thy_ref_merged;
  7.1019    in
  7.1020 -    if T=U then (sign_ref_merged, (t,u)::tpairs)
  7.1021 +    if T=U then (thy_ref_merged, (t,u)::tpairs)
  7.1022      else raise TYPE (Pretty.string_of (Pretty.block [Pretty.str "instantiate: type conflict",
  7.1023 -      Pretty.fbrk, prt_typing sign_ref_merged t T,
  7.1024 -      Pretty.fbrk, prt_typing sign_ref_merged u U]), [T,U], [t,u])
  7.1025 +      Pretty.fbrk, pretty_typing thy_merged t T,
  7.1026 +      Pretty.fbrk, pretty_typing thy_merged u U]), [T,U], [t,u])
  7.1027    end;
  7.1028  
  7.1029 -fun add_ctyp ((Ctyp {T = T as TVar (_, S), sign_ref = sign_refT},
  7.1030 -      Ctyp {T = U, sign_ref = sign_refU}), (sign_ref, vTs)) =
  7.1031 +fun add_ctyp ((Ctyp {T = T as TVar (_, S), thy_ref = thy_refT},
  7.1032 +      Ctyp {T = U, thy_ref = thy_refU}), (thy_ref, vTs)) =
  7.1033        let
  7.1034 -        val sign_ref_merged = Sign.merge_refs
  7.1035 -          (sign_ref, Sign.merge_refs (sign_refT, sign_refU));
  7.1036 -        val sign = Sign.deref sign_ref_merged
  7.1037 +        val thy_ref_merged = Theory.merge_refs
  7.1038 +          (thy_ref, Theory.merge_refs (thy_refT, thy_refU));
  7.1039 +        val thy_merged = Theory.deref thy_ref_merged
  7.1040        in
  7.1041 -        if Type.of_sort (Sign.tsig_of sign) (U, S) then
  7.1042 -          (sign_ref_merged, (T, U) :: vTs)
  7.1043 +        if Type.of_sort (Sign.tsig_of thy_merged) (U, S) then
  7.1044 +          (thy_ref_merged, (T, U) :: vTs)
  7.1045          else raise TYPE ("Type not of sort " ^
  7.1046 -          Sign.string_of_sort sign S, [U], [])
  7.1047 +          Sign.string_of_sort thy_merged S, [U], [])
  7.1048        end
  7.1049 -  | add_ctyp ((Ctyp {T, sign_ref}, _), _) =
  7.1050 +  | add_ctyp ((Ctyp {T, thy_ref}, _), _) =
  7.1051        raise TYPE (Pretty.string_of (Pretty.block
  7.1052          [Pretty.str "instantiate: not a type variable",
  7.1053 -         Pretty.fbrk, prt_type sign_ref T]), [T], []);
  7.1054 +         Pretty.fbrk, Sign.pretty_typ (Theory.deref thy_ref) T]), [T], []);
  7.1055  
  7.1056  in
  7.1057  
  7.1058 @@ -967,18 +974,18 @@
  7.1059    Instantiates distinct Vars by terms of same type.
  7.1060    No longer normalizes the new theorem! *)
  7.1061  fun instantiate ([], []) th = th
  7.1062 -  | instantiate (vcTs,ctpairs) (th as Thm{sign_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) =
  7.1063 -  let val (newsign_ref,tpairs) = foldr add_ctpair (sign_ref,[]) ctpairs;
  7.1064 -      val (newsign_ref,vTs) = foldr add_ctyp (newsign_ref,[]) vcTs;
  7.1065 +  | instantiate (vcTs,ctpairs) (th as Thm{thy_ref,der,maxidx,hyps,shyps,tpairs=dpairs,prop}) =
  7.1066 +  let val (newthy_ref,tpairs) = foldr add_ctpair (thy_ref,[]) ctpairs;
  7.1067 +      val (newthy_ref,vTs) = foldr add_ctyp (newthy_ref,[]) vcTs;
  7.1068        fun subst t =
  7.1069          subst_atomic tpairs (map_term_types (typ_subst_atomic vTs) t);
  7.1070        val newprop = subst prop;
  7.1071        val newdpairs = map (pairself subst) dpairs;
  7.1072        val newth =
  7.1073 -            (Thm{sign_ref = newsign_ref, 
  7.1074 +            (Thm{thy_ref = newthy_ref,
  7.1075                   der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der,
  7.1076                   maxidx = maxidx_of_terms (newprop ::
  7.1077 -                   terms_of_tpairs newdpairs), 
  7.1078 +                   terms_of_tpairs newdpairs),
  7.1079                   shyps = add_insts_sorts ((vTs, tpairs), shyps),
  7.1080                   hyps = hyps,
  7.1081                   tpairs = newdpairs,
  7.1082 @@ -989,7 +996,7 @@
  7.1083        then raise THM("instantiate: type variables not distinct", 0, [th])
  7.1084        else newth
  7.1085    end
  7.1086 -  handle TERM _ => raise THM("instantiate: incompatible signatures", 0, [th])
  7.1087 +  handle TERM _ => raise THM("instantiate: incompatible theories", 0, [th])
  7.1088         | TYPE (msg, _, _) => raise THM (msg, 0, [th]);
  7.1089  
  7.1090  end;
  7.1091 @@ -998,49 +1005,49 @@
  7.1092  (*The trivial implication A==>A, justified by assume and forall rules.
  7.1093    A can contain Vars, not so for assume!   *)
  7.1094  fun trivial ct : thm =
  7.1095 -  let val Cterm {sign_ref, t=A, T, maxidx} = ct
  7.1096 +  let val Cterm {thy_ref, t=A, T, maxidx} = ct
  7.1097    in  if T<>propT then
  7.1098              raise THM("trivial: the term must have type prop", 0, [])
  7.1099        else fix_shyps [] []
  7.1100 -        (Thm{sign_ref = sign_ref, 
  7.1101 +        (Thm{thy_ref = thy_ref,
  7.1102               der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)),
  7.1103 -             maxidx = maxidx, 
  7.1104 -             shyps = [], 
  7.1105 +             maxidx = maxidx,
  7.1106 +             shyps = [],
  7.1107               hyps = [],
  7.1108               tpairs = [],
  7.1109               prop = implies$A$A})
  7.1110    end;
  7.1111  
  7.1112  (*Axiom-scheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *)
  7.1113 -fun class_triv sign c =
  7.1114 -  let val Cterm {sign_ref, t, maxidx, ...} =
  7.1115 -    cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
  7.1116 +fun class_triv thy c =
  7.1117 +  let val Cterm {thy_ref, t, maxidx, ...} =
  7.1118 +    cterm_of thy (Logic.mk_inclass (TVar (("'a", 0), [c]), c))
  7.1119        handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []);
  7.1120    in
  7.1121      fix_shyps [] []
  7.1122 -      (Thm {sign_ref = sign_ref, 
  7.1123 +      (Thm {thy_ref = thy_ref,
  7.1124              der = Pt.infer_derivs' I
  7.1125                (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])),
  7.1126 -            maxidx = maxidx, 
  7.1127 -            shyps = [], 
  7.1128 -            hyps = [], 
  7.1129 +            maxidx = maxidx,
  7.1130 +            shyps = [],
  7.1131 +            hyps = [],
  7.1132              tpairs = [],
  7.1133              prop = t})
  7.1134    end;
  7.1135  
  7.1136  
  7.1137  (* Replace all TFrees not fixed or in the hyps by new TVars *)
  7.1138 -fun varifyT' fixed (Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
  7.1139 +fun varifyT' fixed (Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
  7.1140    let
  7.1141      val tfrees = foldr add_term_tfrees fixed hyps;
  7.1142      val prop1 = attach_tpairs tpairs prop;
  7.1143      val (prop2, al) = Type.varify (prop1, tfrees);
  7.1144      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
  7.1145    in (*no fix_shyps*)
  7.1146 -   (Thm{sign_ref = sign_ref, 
  7.1147 +   (Thm{thy_ref = thy_ref,
  7.1148          der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
  7.1149 -        maxidx = Int.max(0,maxidx), 
  7.1150 -        shyps = shyps, 
  7.1151 +        maxidx = Int.max(0,maxidx),
  7.1152 +        shyps = shyps,
  7.1153          hyps = hyps,
  7.1154          tpairs = rev (map Logic.dest_equals ts),
  7.1155          prop = prop3}, al)
  7.1156 @@ -1049,13 +1056,13 @@
  7.1157  val varifyT = #1 o varifyT' [];
  7.1158  
  7.1159  (* Replace all TVars by new TFrees *)
  7.1160 -fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
  7.1161 +fun freezeT(Thm{thy_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
  7.1162    let
  7.1163      val prop1 = attach_tpairs tpairs prop;
  7.1164      val prop2 = Type.freeze prop1;
  7.1165      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
  7.1166    in (*no fix_shyps*)
  7.1167 -    Thm{sign_ref = sign_ref, 
  7.1168 +    Thm{thy_ref = thy_ref,
  7.1169          der = Pt.infer_derivs' (Pt.freezeT prop1) der,
  7.1170          maxidx = maxidx_of_term prop2,
  7.1171          shyps = shyps,
  7.1172 @@ -1077,27 +1084,27 @@
  7.1173  (*Increment variables and parameters of orule as required for
  7.1174    resolution with goal i of state. *)
  7.1175  fun lift_rule (state, i) orule =
  7.1176 -  let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign_ref=ssign_ref,...} = state
  7.1177 +  let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, thy_ref=sthy_ref,...} = state
  7.1178        val (Bi::_, _) = Logic.strip_prems(i, [], sprop)
  7.1179          handle TERM _ => raise THM("lift_rule", i, [orule,state])
  7.1180 -      val ct_Bi = Cterm {sign_ref=ssign_ref, maxidx=smax, T=propT, t=Bi}
  7.1181 +      val ct_Bi = Cterm {thy_ref=sthy_ref, maxidx=smax, T=propT, t=Bi}
  7.1182        val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1)
  7.1183 -      val (Thm{sign_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule
  7.1184 +      val (Thm{thy_ref, der, maxidx,shyps,hyps,tpairs,prop}) = orule
  7.1185        val (As, B) = Logic.strip_horn prop
  7.1186    in  (*no fix_shyps*)
  7.1187 -      Thm{sign_ref = merge_thm_sgs(state,orule),
  7.1188 +      Thm{thy_ref = merge_thm_thys(state,orule),
  7.1189            der = Pt.infer_derivs' (Pt.lift_proof Bi (smax+1) prop) der,
  7.1190            maxidx = maxidx+smax+1,
  7.1191 -          shyps = Sorts.union_sort(sshyps,shyps), 
  7.1192 -          hyps = hyps, 
  7.1193 +          shyps = Sorts.union_sort(sshyps,shyps),
  7.1194 +          hyps = hyps,
  7.1195            tpairs = map (pairself lift_abs) tpairs,
  7.1196            prop = Logic.list_implies (map lift_all As, lift_all B)}
  7.1197    end;
  7.1198  
  7.1199 -fun incr_indexes i (thm as Thm {sign_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  7.1200 +fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
  7.1201    if i < 0 then raise THM ("negative increment", 0, [thm]) else
  7.1202    if i = 0 then thm else
  7.1203 -    Thm {sign_ref = sign_ref,
  7.1204 +    Thm {thy_ref = thy_ref,
  7.1205           der = Pt.infer_derivs' (Pt.map_proof_terms
  7.1206             (Logic.incr_indexes ([], i)) (incr_tvar i)) der,
  7.1207           maxidx = maxidx + i,
  7.1208 @@ -1108,11 +1115,11 @@
  7.1209  
  7.1210  (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
  7.1211  fun assumption i state =
  7.1212 -  let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
  7.1213 +  let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state;
  7.1214        val (tpairs, Bs, Bi, C) = dest_state(state,i)
  7.1215        fun newth n (env as Envir.Envir{maxidx, ...}, tpairs) =
  7.1216          fix_shyps [state] (env_codT env)
  7.1217 -          (Thm{sign_ref = sign_ref, 
  7.1218 +          (Thm{thy_ref = thy_ref,
  7.1219                 der = Pt.infer_derivs'
  7.1220                   ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
  7.1221                     Pt.assumption_proof Bs Bi n) der,
  7.1222 @@ -1121,7 +1128,7 @@
  7.1223                 hyps = hyps,
  7.1224                 tpairs = if Envir.is_empty env then tpairs else
  7.1225                   map (pairself (Envir.norm_term env)) tpairs,
  7.1226 -               prop = 
  7.1227 +               prop =
  7.1228                 if Envir.is_empty env then (*avoid wasted normalizations*)
  7.1229                     Logic.list_implies (Bs, C)
  7.1230                 else (*normalize the new rule fully*)
  7.1231 @@ -1129,19 +1136,19 @@
  7.1232        fun addprfs [] _ = Seq.empty
  7.1233          | addprfs ((t,u)::apairs) n = Seq.make (fn()=> Seq.pull
  7.1234               (Seq.mapp (newth n)
  7.1235 -                (Unify.unifiers(Sign.deref sign_ref,Envir.empty maxidx, (t,u)::tpairs))
  7.1236 +                (Unify.unifiers(Theory.deref thy_ref,Envir.empty maxidx, (t,u)::tpairs))
  7.1237                  (addprfs apairs (n+1))))
  7.1238    in  addprfs (Logic.assum_pairs (~1,Bi)) 1 end;
  7.1239  
  7.1240  (*Solve subgoal Bi of proof state B1...Bn/C by assumption.
  7.1241    Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
  7.1242  fun eq_assumption i state =
  7.1243 -  let val Thm{sign_ref,der,maxidx,hyps,prop,...} = state;
  7.1244 +  let val Thm{thy_ref,der,maxidx,hyps,prop,...} = state;
  7.1245        val (tpairs, Bs, Bi, C) = dest_state(state,i)
  7.1246    in  (case find_index (op aconv) (Logic.assum_pairs (~1,Bi)) of
  7.1247           (~1) => raise THM("eq_assumption", 0, [state])
  7.1248         | n => fix_shyps [state] []
  7.1249 -                (Thm{sign_ref = sign_ref, 
  7.1250 +                (Thm{thy_ref = thy_ref,
  7.1251                       der = Pt.infer_derivs'
  7.1252                         (Pt.assumption_proof Bs Bi (n+1)) der,
  7.1253                       maxidx = maxidx,
  7.1254 @@ -1154,7 +1161,7 @@
  7.1255  
  7.1256  (*For rotate_tac: fast rotation of assumptions of subgoal i*)
  7.1257  fun rotate_rule k i state =
  7.1258 -  let val Thm{sign_ref,der,maxidx,hyps,prop,shyps,...} = state;
  7.1259 +  let val Thm{thy_ref,der,maxidx,hyps,prop,shyps,...} = state;
  7.1260        val (tpairs, Bs, Bi, C) = dest_state(state,i)
  7.1261        val params = Term.strip_all_vars Bi
  7.1262        and rest   = Term.strip_all_body Bi
  7.1263 @@ -1163,19 +1170,19 @@
  7.1264        val n      = length asms
  7.1265        val m      = if k<0 then n+k else k
  7.1266        val Bi'    = if 0=m orelse m=n then Bi
  7.1267 -		   else if 0<m andalso m<n 
  7.1268 -		   then let val (ps,qs) = splitAt(m,asms)
  7.1269 +                   else if 0<m andalso m<n
  7.1270 +                   then let val (ps,qs) = splitAt(m,asms)
  7.1271                          in list_all(params, Logic.list_implies(qs @ ps, concl))
  7.1272 -			end
  7.1273 -		   else raise THM("rotate_rule", k, [state])
  7.1274 +                        end
  7.1275 +                   else raise THM("rotate_rule", k, [state])
  7.1276    in  (*no fix_shyps*)
  7.1277 -      Thm{sign_ref = sign_ref, 
  7.1278 +      Thm{thy_ref = thy_ref,
  7.1279            der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
  7.1280 -	  maxidx = maxidx,
  7.1281 -	  shyps = shyps,
  7.1282 -	  hyps = hyps,
  7.1283 +          maxidx = maxidx,
  7.1284 +          shyps = shyps,
  7.1285 +          hyps = hyps,
  7.1286            tpairs = tpairs,
  7.1287 -	  prop = Logic.list_implies (Bs @ [Bi'], C)}
  7.1288 +          prop = Logic.list_implies (Bs @ [Bi'], C)}
  7.1289    end;
  7.1290  
  7.1291  
  7.1292 @@ -1183,7 +1190,7 @@
  7.1293    unchanged.  Does nothing if k=0 or if k equals n-j, where n is the
  7.1294    number of premises.  Useful with etac and underlies tactic/defer_tac*)
  7.1295  fun permute_prems j k rl =
  7.1296 -  let val Thm{sign_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl
  7.1297 +  let val Thm{thy_ref,der,maxidx,hyps,tpairs,prop,shyps} = rl
  7.1298        val prems  = Logic.strip_imp_prems prop
  7.1299        and concl  = Logic.strip_imp_concl prop
  7.1300        val moved_prems = List.drop(prems, j)
  7.1301 @@ -1192,18 +1199,18 @@
  7.1302        val n_j    = length moved_prems
  7.1303        val m = if k<0 then n_j + k else k
  7.1304        val prop'  = if 0 = m orelse m = n_j then prop
  7.1305 -		   else if 0<m andalso m<n_j 
  7.1306 -		   then let val (ps,qs) = splitAt(m,moved_prems)
  7.1307 -			in Logic.list_implies(fixed_prems @ qs @ ps, concl) end
  7.1308 -		   else raise THM("permute_prems:k", k, [rl])
  7.1309 +                   else if 0<m andalso m<n_j
  7.1310 +                   then let val (ps,qs) = splitAt(m,moved_prems)
  7.1311 +                        in Logic.list_implies(fixed_prems @ qs @ ps, concl) end
  7.1312 +                   else raise THM("permute_prems:k", k, [rl])
  7.1313    in  (*no fix_shyps*)
  7.1314 -      Thm{sign_ref = sign_ref, 
  7.1315 +      Thm{thy_ref = thy_ref,
  7.1316            der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
  7.1317 -	  maxidx = maxidx,
  7.1318 -	  shyps = shyps,
  7.1319 -	  hyps = hyps,
  7.1320 +          maxidx = maxidx,
  7.1321 +          shyps = shyps,
  7.1322 +          hyps = hyps,
  7.1323            tpairs = tpairs,
  7.1324 -	  prop = prop'}
  7.1325 +          prop = prop'}
  7.1326    end;
  7.1327  
  7.1328  
  7.1329 @@ -1214,7 +1221,7 @@
  7.1330    The names in cs, if distinct, are used for the innermost parameters;
  7.1331     preceding parameters may be renamed to make all params distinct.*)
  7.1332  fun rename_params_rule (cs, i) state =
  7.1333 -  let val Thm{sign_ref,der,maxidx,hyps,shyps,...} = state
  7.1334 +  let val Thm{thy_ref,der,maxidx,hyps,shyps,...} = state
  7.1335        val (tpairs, Bs, Bi, C) = dest_state(state,i)
  7.1336        val iparams = map #1 (Logic.strip_params Bi)
  7.1337        val short = length iparams - length cs
  7.1338 @@ -1225,12 +1232,12 @@
  7.1339        val newBi = Logic.list_rename_params (newnames, Bi)
  7.1340    in
  7.1341    case findrep cs of
  7.1342 -     c::_ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); 
  7.1343 -	      state)
  7.1344 +     c::_ => (warning ("Can't rename.  Bound variables not distinct: " ^ c);
  7.1345 +              state)
  7.1346     | [] => (case cs inter_string freenames of
  7.1347 -       a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); 
  7.1348 -		state)
  7.1349 -     | [] => Thm{sign_ref = sign_ref,
  7.1350 +       a::_ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a);
  7.1351 +                state)
  7.1352 +     | [] => Thm{thy_ref = thy_ref,
  7.1353                   der = der,
  7.1354                   maxidx = maxidx,
  7.1355                   shyps = shyps,
  7.1356 @@ -1242,11 +1249,11 @@
  7.1357  
  7.1358  (*** Preservation of bound variable names ***)
  7.1359  
  7.1360 -fun rename_boundvars pat obj (thm as Thm {sign_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
  7.1361 +fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
  7.1362    (case Term.rename_abs pat obj prop of
  7.1363      NONE => thm
  7.1364    | SOME prop' => Thm
  7.1365 -      {sign_ref = sign_ref,
  7.1366 +      {thy_ref = thy_ref,
  7.1367         der = der,
  7.1368         maxidx = maxidx,
  7.1369         hyps = hyps,
  7.1370 @@ -1280,7 +1287,7 @@
  7.1371                                else Var((y,i),T)
  7.1372                   | NONE=> t)
  7.1373            | rename(Abs(x,T,t)) =
  7.1374 -              Abs(getOpt(assoc_string(al,x),x), T, rename t)
  7.1375 +              Abs (if_none (assoc_string (al, x)) x, T, rename t)
  7.1376            | rename(f$t) = rename f $ rename t
  7.1377            | rename(t) = t;
  7.1378          fun strip_ren Ai = strip_apply rename (Ai,B)
  7.1379 @@ -1332,13 +1339,13 @@
  7.1380  fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted)
  7.1381                          (eres_flg, orule, nsubgoal) =
  7.1382   let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state
  7.1383 -     and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 
  7.1384 +     and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps,
  7.1385               tpairs=rtpairs, prop=rprop,...} = orule
  7.1386           (*How many hyps to skip over during normalization*)
  7.1387       and nlift = Logic.count_prems(strip_all_body Bi,
  7.1388                                     if eres_flg then ~1 else 0)
  7.1389 -     val sign_ref = merge_thm_sgs(state,orule);
  7.1390 -     val sign = Sign.deref sign_ref;
  7.1391 +     val thy_ref = merge_thm_thys(state,orule);
  7.1392 +     val thy = Theory.deref thy_ref;
  7.1393       (** Add new theorem with prop = '[| Bs; As |] ==> C' to thq **)
  7.1394       fun addth A (As, oldAs, rder', n) ((env as Envir.Envir {maxidx, ...}, tpairs), thq) =
  7.1395         let val normt = Envir.norm_term env;
  7.1396 @@ -1357,7 +1364,7 @@
  7.1397                    (ntps, (map normt (Bs @ As), normt C))
  7.1398               end
  7.1399             val th = (*tuned fix_shyps*)
  7.1400 -             Thm{sign_ref = sign_ref,
  7.1401 +             Thm{thy_ref = thy_ref,
  7.1402                   der = Pt.infer_derivs
  7.1403                     ((if Envir.is_empty env then I
  7.1404                       else if Envir.above (smax, env) then
  7.1405 @@ -1390,12 +1397,12 @@
  7.1406       (*elim-resolution: try each assumption in turn.  Initially n=1*)
  7.1407       fun tryasms (_, _, _, []) = Seq.empty
  7.1408         | tryasms (A, As, n, (t,u)::apairs) =
  7.1409 -          (case Seq.pull(Unify.unifiers(sign, env, (t,u)::dpairs))  of
  7.1410 -	      NONE                   => tryasms (A, As, n+1, apairs)
  7.1411 -	    | cell as SOME((_,tpairs),_) =>
  7.1412 -		Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
  7.1413 -		    (Seq.make(fn()=> cell),
  7.1414 -		     Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs)))))
  7.1415 +          (case Seq.pull(Unify.unifiers(thy, env, (t,u)::dpairs))  of
  7.1416 +              NONE                   => tryasms (A, As, n+1, apairs)
  7.1417 +            | cell as SOME((_,tpairs),_) =>
  7.1418 +                Seq.it_right (addth A (newAs(As, n, [BBi,(u,t)], tpairs)))
  7.1419 +                    (Seq.make(fn()=> cell),
  7.1420 +                     Seq.make(fn()=> Seq.pull (tryasms(A, As, n+1, apairs)))))
  7.1421       fun eres [] = raise THM("bicompose: no premises", 0, [orule,state])
  7.1422         | eres (A1::As) = tryasms(SOME A1, As, 1, Logic.assum_pairs(nlift+1,A1))
  7.1423       (*ordinary resolution*)
  7.1424 @@ -1404,7 +1411,7 @@
  7.1425               Seq.it_right (addth NONE (newAs(rev rAs, 0, [BBi], tpairs)))
  7.1426                         (Seq.make (fn()=> cell), Seq.empty)
  7.1427   in  if eres_flg then eres(rev rAs)
  7.1428 -     else res(Seq.pull(Unify.unifiers(sign, env, dpairs)))
  7.1429 +     else res(Seq.pull(Unify.unifiers(thy, env, dpairs)))
  7.1430   end;
  7.1431  end;
  7.1432  
  7.1433 @@ -1442,36 +1449,34 @@
  7.1434  
  7.1435  (*** Oracles ***)
  7.1436  
  7.1437 -fun invoke_oracle_i thy name =
  7.1438 +fun invoke_oracle_i thy1 name =
  7.1439    let
  7.1440 -    val {sign = sg, oracles = (_, oracles), ...} = Theory.rep_theory thy;
  7.1441      val oracle =
  7.1442 -      (case Symtab.lookup (oracles, name) of
  7.1443 +      (case Symtab.lookup (#2 (#oracles (Theory.rep_theory thy1)), name) of
  7.1444          NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
  7.1445        | SOME (f, _) => f);
  7.1446    in
  7.1447 -    fn (sign, exn) =>
  7.1448 +    fn (thy2, data) =>
  7.1449        let
  7.1450 -        val sign_ref' = Sign.merge_refs (Sign.self_ref sg, Sign.self_ref sign);
  7.1451 -        val sign' = Sign.deref sign_ref';
  7.1452 +        val thy' = Theory.merge (thy1, thy2);
  7.1453          val (prop, T, maxidx) =
  7.1454 -          Sign.certify_term (Sign.pp sign') sign' (oracle (sign', exn));
  7.1455 +          Sign.certify_term (Sign.pp thy') thy' (oracle (thy', data));
  7.1456        in
  7.1457          if T <> propT then
  7.1458            raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
  7.1459          else fix_shyps [] []
  7.1460 -          (Thm {sign_ref = sign_ref', 
  7.1461 +          (Thm {thy_ref = Theory.self_ref thy',
  7.1462              der = (true, Pt.oracle_proof name prop),
  7.1463              maxidx = maxidx,
  7.1464 -            shyps = [], 
  7.1465 -            hyps = [], 
  7.1466 +            shyps = [],
  7.1467 +            hyps = [],
  7.1468              tpairs = [],
  7.1469              prop = prop})
  7.1470        end
  7.1471    end;
  7.1472  
  7.1473  fun invoke_oracle thy =
  7.1474 -  invoke_oracle_i thy o NameSpace.intern (#1 (#oracles (Theory.rep_theory thy)));
  7.1475 +  invoke_oracle_i thy o NameSpace.intern (Theory.oracle_space thy);
  7.1476  
  7.1477  
  7.1478  end;
     8.1 --- a/src/Pure/unify.ML	Fri Jun 17 18:33:05 2005 +0200
     8.2 +++ b/src/Pure/unify.ML	Fri Jun 17 18:33:08 2005 +0200
     8.3 @@ -1,33 +1,31 @@
     8.4  (*  Title:      Pure/unify.ML
     8.5      ID:         $Id$
     8.6 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.8      Copyright   Cambridge University 1992
     8.9  
    8.10 -Higher-Order Unification
    8.11 +Higher-Order Unification.
    8.12  
    8.13 -Types as well as terms are unified.  The outermost functions assume the
    8.14 -terms to be unified already have the same type.  In resolution, this is
    8.15 -assured because both have type "prop".
    8.16 +Types as well as terms are unified.  The outermost functions assume
    8.17 +the terms to be unified already have the same type.  In resolution,
    8.18 +this is assured because both have type "prop".
    8.19  *)
    8.20  
    8.21 -
    8.22 -signature UNIFY = 
    8.23 -  sig
    8.24 +signature UNIFY =
    8.25 +sig
    8.26    (*references for control and tracing*)
    8.27    val trace_bound: int ref
    8.28    val trace_simp: bool ref
    8.29    val trace_types: bool ref
    8.30    val search_bound: int ref
    8.31    (*other exports*)
    8.32 -  val combound : (term*int*int) -> term
    8.33 -  val rlist_abs: (string*typ)list * term -> term   
    8.34 -  val smash_unifiers : Sign.sg * Envir.env * (term*term)list
    8.35 -	-> (Envir.env Seq.seq)
    8.36 -  val unifiers: Sign.sg * Envir.env * ((term*term)list)
    8.37 -	-> (Envir.env * (term * term)list) Seq.seq
    8.38 -  end;
    8.39 +  val combound: term * int * int -> term
    8.40 +  val rlist_abs: (string * typ) list * term -> term
    8.41 +  val smash_unifiers: theory * Envir.env * (term * term) list -> Envir.env Seq.seq
    8.42 +  val unifiers: theory * Envir.env * ((term * term) list) ->
    8.43 +    (Envir.env * (term * term) list) Seq.seq
    8.44 +end
    8.45  
    8.46 -structure Unify	: UNIFY = 
    8.47 +structure Unify	: UNIFY =
    8.48  struct
    8.49  
    8.50  (*Unification options*)
    8.51 @@ -38,7 +36,8 @@
    8.52  and trace_types = ref false	(*announce potential incompleteness
    8.53  				  of type unification*)
    8.54  
    8.55 -val sgr = ref(Sign.pre_pure);
    8.56 +val thy_ref = ref (NONE: theory option);
    8.57 +fun thy () = the (! thy_ref);
    8.58  
    8.59  type binderlist = (string*typ) list;
    8.60  
    8.61 @@ -180,12 +179,12 @@
    8.62  
    8.63  fun unify_types(T,U, env as Envir.Envir{asol,iTs,maxidx}) =
    8.64    if T=U then env
    8.65 -  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (!sgr)) (iTs, maxidx) (U, T)
    8.66 +  else let val (iTs',maxidx') = Type.unify (Sign.tsig_of (thy ())) (iTs, maxidx) (U, T)
    8.67         in Envir.Envir{asol=asol,maxidx=maxidx',iTs=iTs'} end
    8.68         handle Type.TUNIFY => raise CANTUNIFY;
    8.69  
    8.70  fun test_unify_types(args as (T,U,_)) =
    8.71 -let val sot = Sign.string_of_typ (!sgr);
    8.72 +let val sot = Sign.string_of_typ (thy ());
    8.73      fun warn() = tracing ("Potential loss of completeness: "^sot U^" = "^sot T);
    8.74      val env' = unify_types(args)
    8.75  in if is_TVar(T) orelse is_TVar(U) then warn() else ();
    8.76 @@ -556,7 +555,7 @@
    8.77      t is always flexible.*)
    8.78  fun print_dpairs msg (env,dpairs) =
    8.79    let fun pdp (rbinder,t,u) =
    8.80 -        let fun termT t = Sign.pretty_term (!sgr)
    8.81 +        let fun termT t = Sign.pretty_term (thy ())
    8.82                                (Envir.norm_term env (rlist_abs(rbinder,t)))
    8.83              val bsymbs = [termT u, Pretty.str" =?=", Pretty.brk 1,
    8.84                            termT t];
    8.85 @@ -567,7 +566,7 @@
    8.86  (*Unify the dpairs in the environment.
    8.87    Returns flex-flex disagreement pairs NOT IN normal form. 
    8.88    SIMPL may raise exception CANTUNIFY. *)
    8.89 -fun hounifiers (sg,env, tus : (term*term)list) 
    8.90 +fun hounifiers (thy,env, tus : (term*term)list) 
    8.91    : (Envir.env * (term*term)list)Seq.seq =
    8.92    let fun add_unify tdepth ((env,dpairs), reseq) =
    8.93  	  Seq.make (fn()=>
    8.94 @@ -591,14 +590,13 @@
    8.95  	    (if tdepth > !trace_bound then tracing"Failure node" else ();
    8.96  	     Seq.pull reseq));
    8.97       val dps = map (fn(t,u)=> ([],t,u)) tus
    8.98 -  in sgr := sg;
    8.99 -     add_unify 1 ((env,dps), Seq.empty) 
   8.100 -  end;
   8.101 +     val _ = thy_ref := SOME thy;
   8.102 +  in add_unify 1 ((env, dps), Seq.empty) end;
   8.103  
   8.104 -fun unifiers(params) =
   8.105 -      Seq.cons((Pattern.unify(params), []),   Seq.empty)
   8.106 -      handle Pattern.Unif => Seq.empty
   8.107 -           | Pattern.Pattern => hounifiers(params);
   8.108 +fun unifiers params =
   8.109 +  Seq.cons ((Pattern.unify params, []), Seq.empty)
   8.110 +    handle Pattern.Unif => Seq.empty
   8.111 +         | Pattern.Pattern => hounifiers params;
   8.112  
   8.113  
   8.114  (*For smash_flexflex1*)
   8.115 @@ -630,7 +628,7 @@
   8.116    foldr smash_flexflex1 env tpairs;
   8.117  
   8.118  (*Returns unifiers with no remaining disagreement pairs*)
   8.119 -fun smash_unifiers (sg, env, tus) : Envir.env Seq.seq =
   8.120 -    Seq.map smash_flexflex (unifiers(sg,env,tus));
   8.121 +fun smash_unifiers (thy, env, tus) : Envir.env Seq.seq =
   8.122 +    Seq.map smash_flexflex (unifiers(thy,env,tus));
   8.123  
   8.124  end;
     9.1 --- a/src/ZF/Datatype.ML	Fri Jun 17 18:33:05 2005 +0200
     9.2 +++ b/src/ZF/Datatype.ML	Fri Jun 17 18:33:08 2005 +0200
     9.3 @@ -73,9 +73,9 @@
     9.4         and (rhead, rargs) = strip_comb rhs
     9.5         val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
     9.6         val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
     9.7 -       val lcon_info = valOf (Symtab.lookup (ConstructorsData.get_sg sg, lname))
     9.8 +       val lcon_info = valOf (Symtab.lookup (ConstructorsData.get sg, lname))
     9.9           handle Option => raise Match;
    9.10 -       val rcon_info = valOf (Symtab.lookup (ConstructorsData.get_sg sg, rname))
    9.11 +       val rcon_info = valOf (Symtab.lookup (ConstructorsData.get sg, rname))
    9.12           handle Option => raise Match;
    9.13         val new = 
    9.14             if #big_rec_name lcon_info = #big_rec_name rcon_info