# HG changeset patch
# User wenzelm
# Date 1119462082 -7200
# Node ID c5744af6b28a6d4670b276025eef918c1334c2b5
# Parent  86c9eada525bad3f1a5b51c90b93a75a14b3d894
renamed init to init_data;

diff -r 86c9eada525b -r c5744af6b28a src/Pure/proofterm.ML
--- 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
diff -r 86c9eada525b -r c5744af6b28a src/Pure/pure_thy.ML
--- 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),
diff -r 86c9eada525b -r c5744af6b28a src/Pure/sign.ML
--- 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);
 
diff -r 86c9eada525b -r c5744af6b28a src/Pure/theory.ML
--- 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);