--- 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 *)