--- a/src/Pure/proofterm.ML Wed Jun 22 19:41:20 2005 +0200
+++ b/src/Pure/proofterm.ML Wed Jun 22 19:41:22 2005 +0200
@@ -107,7 +107,7 @@
(string * (typ list -> proof -> proof option)) list -> proof -> proof
val rewrite_proof_notypes : (proof * proof) list *
(string * (typ list -> proof -> proof option)) list -> proof -> proof
- val init : theory -> theory
+ val init_data: theory -> theory
end
@@ -1107,7 +1107,7 @@
fun print _ _ = ();
end);
-val init = ProofData.init;
+val init_data = ProofData.init;
fun add_prf_rrules rs thy =
let val r = ProofData.get thy
--- a/src/Pure/pure_thy.ML Wed Jun 22 19:41:20 2005 +0200
+++ b/src/Pure/pure_thy.ML Wed Jun 22 19:41:22 2005 +0200
@@ -449,9 +449,9 @@
val proto_pure =
Context.pre_pure_thy
- |> Sign.init
- |> Theory.init
- |> Proofterm.init
+ |> Sign.init_data
+ |> Theory.init_data
+ |> Proofterm.init_data
|> TheoremsData.init
|> Theory.add_types
[("fun", 2, NoSyn),
--- a/src/Pure/sign.ML Wed Jun 22 19:41:20 2005 +0200
+++ b/src/Pure/sign.ML Wed Jun 22 19:41:22 2005 +0200
@@ -72,7 +72,7 @@
sig
type syn
type sg (*obsolete*)
- val init: theory -> theory
+ val init_data: theory -> theory
val rep_sg: theory ->
{naming: NameSpace.naming,
syn: syn,
@@ -238,7 +238,7 @@
fun print _ _ = ();
end);
-val init = SignData.init;
+val init_data = SignData.init;
fun rep_sg thy = SignData.get thy |> (fn Sign args => args);
--- a/src/Pure/theory.ML Wed Jun 22 19:41:20 2005 +0200
+++ b/src/Pure/theory.ML Wed Jun 22 19:41:22 2005 +0200
@@ -33,7 +33,7 @@
val end_theory: theory -> theory
val checkpoint: theory -> theory
val copy: theory -> theory
- val init: theory -> theory
+ val init_data: theory -> theory
val axiom_space: theory -> NameSpace.T
val oracle_space: theory -> NameSpace.T
val axioms_of: theory -> (string * term) list
@@ -135,7 +135,7 @@
structure ThyData = TheoryDataFun
(struct
- val name = "Pure/thy";
+ val name = "Pure/theory";
type T = thy;
val empty = make_thy (NameSpace.empty_table, Defs.empty, NameSpace.empty_table);
val copy = I;
@@ -158,7 +158,7 @@
fun print _ _ = ();
end);
-val init = ThyData.init;
+val init_data = ThyData.init;
fun rep_theory thy = ThyData.get thy |> (fn Thy args => args);