src/Pure/Isar/local_theory.ML
changeset 25289 3d332d8a827c
parent 25120 23fbc38f6432
child 25381 c100bf5bd6b8
--- a/src/Pure/Isar/local_theory.ML	Mon Nov 05 20:50:41 2007 +0100
+++ b/src/Pure/Isar/local_theory.ML	Mon Nov 05 20:50:42 2007 +0100
@@ -41,7 +41,7 @@
   val target_name: local_theory -> bstring -> string
   val init: string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
-  val reinit: local_theory -> theory -> local_theory
+  val reinit: local_theory -> local_theory
   val exit: local_theory -> Proof.context
 end;
 
@@ -67,7 +67,7 @@
   term_syntax: declaration -> local_theory -> local_theory,
   declaration: declaration -> local_theory -> local_theory,
   target_naming: local_theory -> NameSpace.naming,
-  reinit: local_theory -> theory -> local_theory,
+  reinit: local_theory -> local_theory,
   exit: local_theory -> Proof.context};
 
 datatype lthy = LThy of