# HG changeset patch
# User wenzelm
# Date 1194292242 -3600
# Node ID 3d332d8a827c77cb4f779129ff80007bc69be9e0
# Parent  6e0c8dd213df9a8b85f3a1473e7e063cf7b1661c
simplified LocalTheory.reinit;

diff -r 6e0c8dd213df -r 3d332d8a827c src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Nov 05 20:50:41 2007 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Nov 05 20:50:42 2007 +0100
@@ -306,7 +306,7 @@
     lthy
       |> FundefPackage.add_fundef fixes statements config flags
       |> by_pat_completeness_simp
-      |> (fn lthy => LocalTheory.reinit lthy (ProofContext.theory_of lthy))
+      |> LocalTheory.reinit
       |> termination_by_lexicographic_order
 
 val _ =
diff -r 6e0c8dd213df -r 3d332d8a827c src/Pure/Isar/local_theory.ML
--- 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
diff -r 6e0c8dd213df -r 3d332d8a827c src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Mon Nov 05 20:50:41 2007 +0100
+++ b/src/Pure/Isar/subclass.ML	Mon Nov 05 20:50:42 2007 +0100
@@ -38,7 +38,7 @@
       |> map (ObjectLogic.ensure_propT thy);
     fun after_qed thms =
       LocalTheory.theory (Class.prove_subclass (sub, sup) thms ctxt)
-      #> (fn lthy => LocalTheory.reinit lthy (ProofContext.theory_of (LocalTheory.target_of lthy)));
+      #> LocalTheory.reinit;
   in
     do_proof after_qed sublocale_prop lthy
   end;