# HG changeset patch
# User wenzelm
# Date 1231326502 -3600
# Node ID a9ee3475abf411c7ecafc9b923f4a2c2f1d0be19
# Parent  f65670092259507bca6cf6da916e554c366e0dac
added local_theory';

diff -r f65670092259 -r a9ee3475abf4 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Jan 07 08:04:12 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jan 07 12:08:22 2009 +0100
@@ -17,6 +17,8 @@
   val improper_command: string -> string -> OuterKeyword.T ->
     (Toplevel.transition -> Toplevel.transition) parser -> unit
   val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
+  val local_theory': string -> string -> OuterKeyword.T ->
+    (bool -> local_theory -> local_theory) parser -> unit
   val local_theory: string -> string -> OuterKeyword.T ->
     (local_theory -> local_theory) parser -> unit
   val local_theory_to_proof': string -> string -> OuterKeyword.T ->
@@ -138,6 +140,7 @@
   command name comment kind (P.opt_target -- parse
     >> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
 
+val local_theory' = local_theory_command false Toplevel.local_theory';
 val local_theory = local_theory_command false Toplevel.local_theory;
 val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
 val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
diff -r f65670092259 -r a9ee3475abf4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Jan 07 08:04:12 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Jan 07 12:08:22 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/toplevel.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Isabelle/Isar toplevel transactions.
@@ -66,6 +65,8 @@
   val theory': (bool -> theory -> theory) -> transition -> transition
   val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
   val end_local_theory: transition -> transition
+  val local_theory': xstring option -> (bool -> local_theory -> local_theory) ->
+    transition -> transition
   val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition
   val present_local_theory: xstring option -> (node -> unit) -> transition -> transition
   val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) ->
@@ -512,14 +513,15 @@
   (fn Theory (gthy, _) =>
         let
           val finish = loc_finish loc gthy;
-          val lthy' = f (loc_begin loc gthy);
+          val lthy' = f int (loc_begin loc gthy);
         in Theory (finish lthy', SOME lthy') end
     | _ => raise UNDEF) #> tap g);
 
 in
 
-fun local_theory loc f = local_theory_presentation loc f (K I);
-fun present_local_theory loc g = local_theory_presentation loc I g;
+fun local_theory' loc f = local_theory_presentation loc f (K I);
+fun local_theory loc f = local_theory' loc (K f);
+fun present_local_theory loc g = local_theory_presentation loc (K I) g;
 
 end;