# HG changeset patch
# User haftmann
# Date 1281539967 -7200
# Node ID 7d1e2a6831ecd88a8feaf76cbe9f73095a2472f5
# Parent  cf42d8355844719b3ab476f35dc6e845b2402387
remove reinit operation alltogether

diff -r cf42d8355844 -r 7d1e2a6831ec src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Aug 11 17:16:02 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed Aug 11 17:19:27 2010 +0200
@@ -597,7 +597,6 @@
       declaration = K Generic_Target.theory_declaration,
       syntax_declaration = K Generic_Target.theory_declaration,
       pretty = single o pretty_instantiation,
-      reinit = instantiation arities o ProofContext.theory_of,
       exit = Local_Theory.target_of o conclude_instantiation};
 
 fun instantiation_cmd arities thy =
diff -r cf42d8355844 -r 7d1e2a6831ec src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Aug 11 17:16:02 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Aug 11 17:19:27 2010 +0200
@@ -50,7 +50,6 @@
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: serial option -> string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
-  val reinit: local_theory -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
@@ -75,7 +74,6 @@
   declaration: bool -> declaration -> local_theory -> local_theory,
   syntax_declaration: bool -> declaration -> local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list,
-  reinit: local_theory -> local_theory,
   exit: local_theory -> Proof.context};
 
 datatype lthy = LThy of
@@ -260,8 +258,6 @@
   let val {naming, theory_prefix, operations, target} = get_lthy lthy
   in init (Name_Space.get_group naming) theory_prefix operations target end;
 
-val reinit = checkpoint o operation #reinit;
-
 
 (* exit *)
 
diff -r cf42d8355844 -r 7d1e2a6831ec src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Aug 11 17:16:02 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Aug 11 17:19:27 2010 +0200
@@ -196,7 +196,6 @@
       syntax_declaration = fn pervasive => target_declaration ta
         { syntax = true, pervasive = pervasive },
       pretty = pretty ta,
-      reinit = init_target ta o ProofContext.theory_of,
       exit = Local_Theory.target_of};
 
 in
diff -r cf42d8355844 -r 7d1e2a6831ec src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Aug 11 17:16:02 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 17:19:27 2010 +0200
@@ -218,7 +218,6 @@
         declaration = K Generic_Target.theory_declaration,
         syntax_declaration = K Generic_Target.theory_declaration,
         pretty = single o pretty,
-        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
         exit = Local_Theory.target_of o conclude}
   end;