src/Pure/theory.ML
changeset 16495 2e99aca906a7
parent 16443 82a116532e3e
child 16536 c5744af6b28a
     1.1 --- a/src/Pure/theory.ML	Mon Jun 20 22:14:08 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Mon Jun 20 22:14:09 2005 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    type theory
     1.6    type theory_ref
     1.7 -  val sign_of: theory -> theory    (*dummy*)
     1.8 +  val sign_of: theory -> theory    (*obsolete*)
     1.9    val rep_theory: theory ->
    1.10     {axioms: term NameSpace.table,
    1.11      defs: Defs.graph,
    1.12 @@ -29,6 +29,10 @@
    1.13  sig
    1.14    include BASIC_THEORY
    1.15    include SIGN_THEORY
    1.16 +  val begin_theory: string -> theory list -> theory
    1.17 +  val end_theory: theory -> theory
    1.18 +  val checkpoint: theory -> theory
    1.19 +  val copy: theory -> theory
    1.20    val init: theory -> theory
    1.21    val axiom_space: theory -> NameSpace.T
    1.22    val oracle_space: theory -> NameSpace.T
    1.23 @@ -40,8 +44,6 @@
    1.24    val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
    1.25    val requires: theory -> string -> string -> unit
    1.26    val assert_super: theory -> theory -> theory
    1.27 -  val copy: theory -> theory
    1.28 -  val checkpoint: theory -> theory
    1.29    val add_axioms: (bstring * string) list -> theory -> theory
    1.30    val add_axioms_i: (bstring * term) list -> theory -> theory
    1.31    val add_defs: bool -> (bstring * string) list -> theory -> theory
    1.32 @@ -49,7 +51,7 @@
    1.33    val add_finals: bool -> string list -> theory -> theory
    1.34    val add_finals_i: bool -> term list -> theory -> theory
    1.35    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
    1.36 -end;
    1.37 +end
    1.38  
    1.39  structure Theory: THEORY =
    1.40  struct
    1.41 @@ -63,8 +65,6 @@
    1.42  
    1.43  val eq_thy = Context.eq_thy;
    1.44  val subthy = Context.subthy;
    1.45 -val copy = Context.copy_thy;
    1.46 -val checkpoint = Context.checkpoint_thy;
    1.47  
    1.48  val parents_of = Context.parents_of;
    1.49  val ancestors_of = Context.ancestors_of;
    1.50 @@ -74,6 +74,11 @@
    1.51  val merge = Context.merge;
    1.52  val merge_refs = Context.merge_refs;
    1.53  
    1.54 +val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;
    1.55 +val end_theory = Context.finish_thy;
    1.56 +val checkpoint = Context.checkpoint_thy;
    1.57 +val copy = Context.copy_thy;
    1.58 +
    1.59  
    1.60  (* signature operations *)
    1.61