# HG changeset patch
# User huffman
# Date 1231478020 28800
# Node ID 85bc8b63747c24f74f32d72139c5718ff62b5e3d
# Parent  97916a925a69682228278ee5d5a655747ef86d5c# Parent  89813bbf0f3e8bdd14826fade4c36137180e37a0
merged.

diff -r 97916a925a69 -r 85bc8b63747c CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Jan 08 12:25:22 2009 -0800
+++ b/CONTRIBUTORS	Thu Jan 08 21:13:40 2009 -0800
@@ -7,12 +7,19 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* December 2008: Clemens Ballarin, TUM
+  New locale implementation.
+
 * December 2008: Armin Heller, TUM and Alexander Krauss, TUM
   Method "sizechange" for advanced termination proofs.
 
 * November 2008: Timothy Bourke, NICTA
   Performance improvement (factor 50) for find_theorems.
 
+* 2008: Florian Haftmann, TUM
+  Various extensions and restructurings in HOL, improvements
+  in evaluation mechanisms, new module binding.ML for name bindings.
+
 * October 2008: Fabian Immler, TUM
   ATP manager for Sledgehammer, based on ML threads instead of Posix
   processes.  Additional ATP wrappers, including remote SystemOnTPTP
diff -r 97916a925a69 -r 85bc8b63747c NEWS
--- a/NEWS	Thu Jan 08 12:25:22 2009 -0800
+++ b/NEWS	Thu Jan 08 21:13:40 2009 -0800
@@ -236,6 +236,13 @@
     src/HOL/Real/rat_arith.ML ~> src/HOL/Tools
     src/HOL/Real/real_arith.ML ~> src/HOL/Tools
 
+    src/HOL/Library/Array.thy ~> src/HOL/Imperative_HOL
+    src/HOL/Library/Heap_Monad.thy ~> src/HOL/Imperative_HOL
+    src/HOL/Library/Heap.thy ~> src/HOL/Imperative_HOL
+    src/HOL/Library/Imperative_HOL.thy ~> src/HOL/Imperative_HOL
+    src/HOL/Library/Ref.thy ~> src/HOL/Imperative_HOL
+    src/HOL/Library/Relational.thy ~> src/HOL/Imperative_HOL
+
 * If methods "eval" and "evaluation" encounter a structured proof state
 with !!/==>, only the conclusion is evaluated to True (if possible),
 avoiding strange error messages.
diff -r 97916a925a69 -r 85bc8b63747c doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/doc-src/more_antiquote.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -50,7 +50,7 @@
   end
 
 
-(* class antiquotation *)
+(* class and type constructor antiquotation *)
 
 local
 
@@ -74,6 +74,38 @@
 end;
 
 
+(* code theorem antiquotation *)
+
+local
+
+fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t;
+
+fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
+
+fun no_vars ctxt thm =
+  let
+    val ctxt' = Variable.set_body false ctxt;
+    val ((_, [thm]), _) = Variable.import_thms true [thm] ctxt';
+  in thm end;
+
+fun pretty_code_thm src ctxt raw_const =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val const = Code_Unit.check_const thy raw_const;
+    val (_, funcgr) = Code_Funcgr.make thy [const];
+    val thms = Code_Funcgr.eqns funcgr const
+      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
+      |> map (no_vars ctxt o AxClass.overload thy);
+  in ThyOutput.output_list pretty_thm src ctxt thms end;
+
+in
+
+val _ = O.add_commands
+  [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
+
+end;
+
+
 (* code antiquotation *)
 
 local
diff -r 97916a925a69 -r 85bc8b63747c src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/HOL/Statespace/state_space.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -160,7 +160,7 @@
 
 fun add_locale_cmd name expr elems thy =
   thy 
-  |> Expression.add_locale_cmd name name expr elems
+  |> Expression.add_locale_cmd name "" expr elems
   |> snd
   |> LocalTheory.exit;
 
diff -r 97916a925a69 -r 85bc8b63747c src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -199,14 +199,14 @@
 fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt)
 
 val by_pat_completeness_simp =
-    Proof.future_terminal_proof
+    Proof.global_future_terminal_proof
       (Method.Basic (pat_completeness, Position.none),
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
-fun termination_by method =
+fun termination_by method int =
     FundefPackage.setup_termination_proof NONE
-    #> Proof.future_terminal_proof
-      (Method.Basic (method, Position.none), NONE)
+    #> Proof.global_future_terminal_proof
+      (Method.Basic (method, Position.none), NONE) int
 
 fun mk_catchall fixes arities =
     let
@@ -304,19 +304,19 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-fun fun_cmd config fixes statements flags lthy =
+fun fun_cmd config fixes statements flags int lthy =
   let val group = serial_string () in
     lthy
       |> LocalTheory.set_group group
       |> FundefPackage.add_fundef fixes statements config flags
-      |> by_pat_completeness_simp
+      |> by_pat_completeness_simp int
       |> LocalTheory.restore
       |> LocalTheory.set_group group
-      |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy))
+      |> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) int
   end;
 
 val _ =
-  OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl
+  OuterSyntax.local_theory' "fun" "define general recursive functions (short version)" K.thy_decl
   (fundef_parser fun_config
      >> (fn ((config, fixes), (flags, statements)) => fun_cmd config fixes statements flags));
 
diff -r 97916a925a69 -r 85bc8b63747c src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/HOL/Tools/res_axioms.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -456,7 +456,7 @@
           |> fold (mark_seen o #1) new_facts
           |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms)
           |>> map_filter I;
-        val cache_entries = ParList.map skolem_cnfs defs;
+        val cache_entries = Par_List.map skolem_cnfs defs;
       in SOME (fold update_cache cache_entries thy') end
   end;
 
diff -r 97916a925a69 -r 85bc8b63747c src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/HOL/ex/ROOT.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -11,12 +11,14 @@
   "Word",
   "Eval_Examples",
   "Quickcheck",
-  "Term_Of_Syntax"
+  "Term_Of_Syntax",
+  "Codegenerator",
+  "Codegenerator_Pretty",
+  "NormalForm",
+  "../NumberTheory/Factorization",
+  "../Library/BigO"
 ];
 
-no_document use_thy "Codegenerator";
-no_document use_thy "Codegenerator_Pretty";
-
 use_thys [
   "Numeral",
   "ImperativeQuicksort",
@@ -57,56 +59,43 @@
   "Meson_Test",
   "Code_Antiq",
   "Termination",
-  "Coherent"
+  "Coherent",
+  "Dense_Linear_Order_Ex",
+  "PresburgerEx",
+  "Reflected_Presburger",
+  "Reflection",
+  "ReflectionEx",
+  "BinEx",
+  "Sqrt",
+  "Sqrt_Script",
+  "BigO_Complex",
+  "Arithmetic_Series_Complex",
+  "HarmonicSeries",
+  "MIR",
+  "ReflectedFerrack",
+  "Refute_Examples",
+  "Quickcheck_Examples"
 ];
 
-setmp Proofterm.proofs 2 time_use_thy "Hilbert_Classical";
+setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";
 
-time_use_thy "Dense_Linear_Order_Ex";
-time_use_thy "PresburgerEx";
-time_use_thy "Reflected_Presburger";
 
-use_thys ["Reflection", "ReflectionEx"];
+use_thy "SVC_Oracle";
 
-time_use_thy "SVC_Oracle";
-
-(*check if user has SVC installed*)
 fun svc_enabled () = getenv "SVC_HOME" <> "";
 fun if_svc_enabled f x = if svc_enabled () then f x else ();
 
-if_svc_enabled time_use_thy "svc_test";
+if_svc_enabled use_thy "svc_test";
+
 
 (* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
 (* installed:                                                       *)
-try time_use_thy "SAT_Examples";
+try use_thy "SAT_Examples";
 
 (* requires zChaff (or some other reasonably fast SAT solver) to be *)
 (* installed:                                                       *)
 if getenv "ZCHAFF_HOME" <> "" then
-  time_use_thy "Sudoku"
+  use_thy "Sudoku"
 else ();
 
-time_use_thy "Refute_Examples";
-time_use_thy "Quickcheck_Examples";
-no_document time_use_thy "NormalForm";
-
 HTML.with_charset "utf-8" (no_document use_thys) ["Hebrew", "Chinese"];
-
-no_document use_thys [
-  "../NumberTheory/Factorization",
-  "../Library/BigO"
-];
-
-use_thys [
-  "BinEx",
-  "Sqrt",
-  "Sqrt_Script",
-  "BigO_Complex",
-
-  "Arithmetic_Series_Complex",
-  "HarmonicSeries",
-
-  "MIR",
-  "ReflectedFerrack"
-];
-
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Concurrent/future.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -137,15 +137,17 @@
   change workers (AList.update Thread.equal (Thread.self (), active));
 
 
-(* execute *)
+(* execute jobs *)
 
 fun do_cancel group = (*requires SYNCHRONIZED*)
   change canceled (insert Task_Queue.eq_group group);
 
-fun execute name (task, group, run) =
+fun execute name (task, group, jobs) =
   let
     val _ = trace_active ();
-    val ok = setmp_thread_data (name, task) run ();
+    val valid = Task_Queue.is_valid group;
+    val ok = setmp_thread_data (name, task) (fn () =>
+      fold (fn job => fn ok => job valid andalso ok) jobs true) ();
     val _ = SYNCHRONIZED "execute" (fn () =>
      (change queue (Task_Queue.finish task);
       if ok then ()
@@ -225,16 +227,15 @@
   else ());
 
 
-(* future values: fork independent computation *)
+
+(** futures **)
 
-fun future opt_group deps pri (e: unit -> 'a) =
+(* future job: fill result *)
+
+fun future_job group (e: unit -> 'a) =
   let
-    val _ = scheduler_check "future check";
-
-    val group = (case opt_group of SOME group => group | NONE => Task_Queue.new_group ());
-
     val result = ref (NONE: 'a Exn.result option);
-    val run = Multithreading.with_attributes (Thread.getAttributes ())
+    val job = Multithreading.with_attributes (Thread.getAttributes ())
       (fn _ => fn ok =>
         let
           val res = if ok then Exn.capture e () else Exn.Exn Exn.Interrupt;
@@ -245,63 +246,91 @@
             | Exn.Exn Exn.Interrupt => (Task_Queue.invalidate_group group; true)
             | _ => false);
         in res_ok end);
+  in (result, job) end;
 
+
+(* fork *)
+
+fun fork_future opt_group deps pri e =
+  let
+    val _ = scheduler_check "future check";
+
+    val group = (case opt_group of SOME group => group | NONE => Task_Queue.new_group ());
+    val (result, job) = future_job group e;
     val task = SYNCHRONIZED "future" (fn () =>
-      change_result queue (Task_Queue.enqueue group deps pri run) before notify_all ());
+      change_result queue (Task_Queue.enqueue group deps pri job) before notify_all ());
   in Future {task = task, group = group, result = result} end;
 
-fun fork e = future NONE [] 0 e;
-fun fork_group group e = future (SOME group) [] 0 e;
-fun fork_deps deps e = future NONE (map task_of deps) 0 e;
-fun fork_pri pri e = future NONE [] pri e;
+fun fork e = fork_future NONE [] 0 e;
+fun fork_group group e = fork_future (SOME group) [] 0 e;
+fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
+fun fork_pri pri e = fork_future NONE [] pri e;
 
 
-(* join: retrieve results *)
+(* join *)
+
+fun get_result x = the_default (Exn.Exn (SYS_ERROR "unfinished future")) (peek x);
 
-fun join_results [] = []
-  | join_results xs = uninterruptible (fn _ => fn () =>
-      let
-        val _ = scheduler_check "join check";
-        val _ = Multithreading.self_critical () andalso
-          exists (not o is_finished) xs andalso
-          error "Cannot join future values within critical section";
+fun join_results xs =
+  if forall is_finished xs then map get_result xs
+  else uninterruptible (fn _ => fn () =>
+    let
+      val _ = scheduler_check "join check";
+      val _ = Multithreading.self_critical () andalso
+        error "Cannot join future values within critical section";
 
-        fun join_loop _ [] = ()
-          | join_loop name tasks =
-              (case SYNCHRONIZED name (fn () =>
-                  change_result queue (Task_Queue.dequeue_towards tasks)) of
-                NONE => ()
-              | SOME (work, tasks') => (execute name work; join_loop name tasks'));
-        val _ =
-          (case thread_data () of
-            NONE =>
-              (*alien thread -- refrain from contending for resources*)
-              while exists (not o is_finished) xs
-              do SYNCHRONIZED "join_thread" (fn () => wait ())
-          | SOME (name, task) =>
-              (*proper task -- actively work towards results*)
-              let
-                val unfinished = xs |> map_filter
-                  (fn Future {task, result = ref NONE, ...} => SOME task | _ => NONE);
-                val _ = SYNCHRONIZED "join" (fn () =>
-                  (change queue (Task_Queue.depend unfinished task); notify_all ()));
-                val _ = join_loop ("join_loop: " ^ name) unfinished;
-                val _ =
-                  while exists (not o is_finished) xs
-                  do SYNCHRONIZED "join_task" (fn () => worker_wait ());
-              in () end);
+      fun join_loop _ [] = ()
+        | join_loop name deps =
+            (case SYNCHRONIZED name (fn () =>
+                change_result queue (Task_Queue.dequeue_towards deps)) of
+              NONE => ()
+            | SOME (work, deps') => (execute name work; join_loop name deps'));
+      val _ =
+        (case thread_data () of
+          NONE =>
+            (*alien thread -- refrain from contending for resources*)
+            while not (forall is_finished xs)
+            do SYNCHRONIZED "join_thread" (fn () => wait ())
+        | SOME (name, task) =>
+            (*proper task -- actively work towards results*)
+            let
+              val pending = filter_out is_finished xs;
+              val deps = map task_of pending;
+              val _ = SYNCHRONIZED "join" (fn () =>
+                (change queue (Task_Queue.depend deps task); notify_all ()));
+              val _ = join_loop ("join_loop: " ^ name) deps;
+              val _ =
+                while not (forall is_finished pending)
+                do SYNCHRONIZED "join_task" (fn () => worker_wait ());
+            in () end);
 
-      in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) ();
+    in map get_result xs end) ();
 
 fun join_result x = singleton join_results x;
 fun join x = Exn.release (join_result x);
 
-fun map f x =
-  let val task = task_of x
-  in future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x)) end;
+
+(* map *)
+
+fun map_future f x =
+  let
+    val _ = scheduler_check "map_future check";
+
+    val task = task_of x;
+    val group = Task_Queue.new_group ();
+    val (result, job) = future_job group (fn () => f (join x));
+
+    val extended = SYNCHRONIZED "map_future" (fn () =>
+      (case Task_Queue.extend task job (! queue) of
+        SOME queue' => (queue := queue'; true)
+      | NONE => false));
+  in
+    if extended then Future {task = task, group = group, result = result}
+    else fork_future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x))
+  end;
 
 
-(* misc operations *)
+(* cancel *)
 
 (*interrupt: permissive signal, may get ignored*)
 fun interrupt_task id = SYNCHRONIZED "interrupt"
@@ -313,7 +342,9 @@
   SYNCHRONIZED "cancel" (fn () => (do_cancel (group_of x); notify_all ())));
 
 
-(*global join and shutdown*)
+
+(** global join and shutdown **)
+
 fun shutdown () =
   if Multithreading.available then
    (scheduler_check "shutdown check";
@@ -327,6 +358,10 @@
       OS.Process.sleep (Time.fromMilliseconds 300))))
   else ();
 
+
+(*final declarations of this structure!*)
+val map = map_future;
+
 end;
 
 type 'a future = 'a Future.future;
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Concurrent/par_list.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Concurrent/par_list.ML
-    ID:         $Id$
     Author:     Makarius
 
 Parallel list combinators.
@@ -24,7 +23,7 @@
   val forall: ('a -> bool) -> 'a list -> bool
 end;
 
-structure ParList: PAR_LIST =
+structure Par_List: PAR_LIST =
 struct
 
 fun raw_map f xs =
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Concurrent/par_list_dummy.ML
--- a/src/Pure/Concurrent/par_list_dummy.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Concurrent/par_list_dummy.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -1,11 +1,10 @@
 (*  Title:      Pure/Concurrent/par_list_dummy.ML
-    ID:         $Id$
     Author:     Makarius
 
 Dummy version of parallel list combinators -- plain sequential evaluation.
 *)
 
-structure ParList: PAR_LIST =
+structure Par_List: PAR_LIST =
 struct
 
 val map = map;
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Concurrent/task_queue.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -13,16 +13,18 @@
   type group
   val eq_group: group * group -> bool
   val new_group: unit -> group
+  val is_valid: group -> bool
   val invalidate_group: group -> unit
   val str_of_group: group -> string
   type queue
   val empty: queue
   val is_empty: queue -> bool
   val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
+  val extend: task -> (bool -> bool) -> queue -> queue option
   val depend: task list -> task -> queue -> queue
-  val dequeue: queue -> (task * group * (unit -> bool)) option * queue
+  val dequeue: queue -> (task * group * (bool -> bool) list) option * queue
   val dequeue_towards: task list -> queue ->
-    (((task * group * (unit -> bool)) * task list) option * queue)
+    (((task * group * (bool -> bool) list) * task list) option * queue)
   val interrupt: queue -> task -> unit
   val interrupt_external: queue -> string -> unit
   val cancel: queue -> group -> bool
@@ -52,6 +54,7 @@
 
 fun new_group () = Group (serial (), ref true);
 
+fun is_valid (Group (_, ref ok)) = ok;
 fun invalidate_group (Group (_, ok)) = ok := false;
 
 fun str_of_group (Group (i, ref ok)) =
@@ -61,14 +64,14 @@
 (* jobs *)
 
 datatype job =
-  Job of bool -> bool |
+  Job of (bool -> bool) list |
   Running of Thread.thread;
 
 type jobs = (group * job) Task_Graph.T;
 
 fun get_group (jobs: jobs) task = #1 (Task_Graph.get_node jobs task);
 fun get_job (jobs: jobs) task = #2 (Task_Graph.get_node jobs task);
-fun map_job task f (jobs: jobs) = Task_Graph.map_node task (apsnd f) jobs;
+fun set_job task job (jobs: jobs) = Task_Graph.map_node task (fn (group, _) => (group, job)) jobs;
 
 fun add_job task dep (jobs: jobs) =
   Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
@@ -96,9 +99,14 @@
     val task = new_task pri;
     val groups' = Inttab.cons_list (gid, task) groups;
     val jobs' = jobs
-      |> Task_Graph.new_node (task, (group, Job job)) |> fold (add_job task) deps;
+      |> Task_Graph.new_node (task, (group, Job [job])) |> fold (add_job task) deps;
   in (task, make_queue groups' jobs') end;
 
+fun extend task job (Queue {groups, jobs}) =
+  (case try (get_job jobs) task of
+    SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs))
+  | _ => NONE);
+
 fun depend deps task (Queue {groups, jobs}) =
   make_queue groups (fold (add_job_acyclic task) deps jobs);
 
@@ -109,14 +117,13 @@
 
 fun dequeue_result NONE queue = (NONE, queue)
   | dequeue_result (SOME (result as (task, _, _))) (Queue {groups, jobs}) =
-      (SOME result, make_queue groups (map_job task (K (Running (Thread.self ()))) jobs));
+      (SOME result, make_queue groups (set_job task (Running (Thread.self ())) jobs));
 
 in
 
 fun dequeue (queue as Queue {jobs, ...}) =
   let
-    fun ready (task, ((group as Group (_, ref ok), Job job), ([], _))) =
-          SOME (task, group, (fn () => job ok))
+    fun ready (task, ((group, Job list), ([], _))) = SOME (task, group, rev list)
       | ready _ = NONE;
   in dequeue_result (Task_Graph.get_first ready jobs) queue end;
 
@@ -126,8 +133,8 @@
 
     fun ready task =
       (case Task_Graph.get_node jobs task of
-        (group as Group (_, ref ok), Job job) =>
-          if null (Task_Graph.imm_preds jobs task) then SOME (task, group, (fn () => job ok))
+        (group, Job list) =>
+          if null (Task_Graph.imm_preds jobs task) then SOME (task, group, rev list)
           else NONE
       | _ => NONE);
   in
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/class.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -11,9 +11,9 @@
       ML is artificial*)
 
   val class: bstring -> class list -> Element.context_i list
-    -> theory -> string * Proof.context
+    -> theory -> string * local_theory
   val class_cmd: bstring -> xstring list -> Element.context list
-    -> theory -> string * Proof.context
+    -> theory -> string * local_theory
   val prove_subclass: tactic -> class -> local_theory -> local_theory
   val subclass: class -> local_theory -> Proof.state
   val subclass_cmd: xstring -> local_theory -> Proof.state
@@ -208,7 +208,7 @@
         register class sups params base_sort inst
           morphism axiom assm_intro of_class
     #> fold (note_assm_intro class) (the_list assm_intro))))))
-    |> init class
+    |> TheoryTarget.init (SOME class)
     |> pair class
   end;
 
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/expression.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -18,9 +18,9 @@
     Proof.context -> (term * term list) list list * Proof.context;
 
   (* Declaring locales *)
-  val add_locale: string -> bstring -> expression_i -> Element.context_i list ->
+  val add_locale: bstring -> bstring -> expression_i -> Element.context_i list ->
     theory -> string * local_theory;
-  val add_locale_cmd: string -> bstring -> expression -> Element.context list ->
+  val add_locale_cmd: bstring -> bstring -> expression -> Element.context list ->
     theory -> string * local_theory;
 
   (* Interpretation *)
@@ -698,18 +698,20 @@
   | defines_to_notes _ e = e;
 
 fun gen_add_locale prep_decl
-    bname predicate_name raw_imprt raw_body thy =
+    bname raw_predicate_bname raw_imprt raw_body thy =
   let
     val name = Sign.full_bname thy bname;
-    val _ = Locale.test_locale thy name andalso
+    val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
     val ((fixed, deps, body_elems), (parms, ctxt')) =
       prep_decl raw_imprt raw_body (ProofContext.init thy);
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
+    val predicate_bname = if raw_predicate_bname = "" then bname
+      else raw_predicate_bname;
     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
-      define_preds predicate_name parms text thy;
+      define_preds predicate_bname parms text thy;
 
     val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
     val _ = if null extraTs then ()
@@ -787,7 +789,7 @@
         fold store_dep (deps ~~ prep_result propss results) #>
         (* propagate registrations *)
         (fn thy => fold_rev (fn reg => Locale.activate_global_facts reg)
-          (Locale.get_global_registrations thy) thy));
+          (Locale.get_registrations thy) thy));
   in
     goal_ctxt |>
       Proof.theorem_i NONE after_qed (prep_propp propss) |>
@@ -824,7 +826,7 @@
         let
           val thms' = map (Element.morph_witness export') thms;
           val morph' = morph $> Element.satisfy_morphism thms';
-          val add = Locale.add_global_registration (name, (morph', export));
+          val add = Locale.add_registration (name, (morph', export));
         in ((name, morph') :: regs, add thy) end
       | store (Eqns [], []) (regs, thy) =
         let val add = fold_rev (fn (name, morph) =>
@@ -842,7 +844,7 @@
           val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns;
           val add =
             fold_rev (fn (name, morph) =>
-              Locale.amend_global_registration eq_morph (name, morph) #>
+              Locale.amend_registration eq_morph (name, morph) #>
               Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs #>
             PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #>
             snd
@@ -887,7 +889,7 @@
       end;
 
     fun after_qed results =
-      Proof.map_context (fold store_reg (regs ~~ prep_result propss results)) #> Seq.single;
+      Proof.map_context (fold store_reg (regs ~~ prep_result propss results));
   in
     state |> Proof.map_context (K goal_ctxt) |>
       Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/isar.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -133,11 +133,12 @@
     (case Source.get_single (Source.set_prompt Source.default_prompt src) of
       NONE => if secure then quit () else ()
     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
-    handle exn => (Output.error_msg (Toplevel.exn_message exn)
-    handle crash =>
-      (CRITICAL (fn () => change crashes (cons crash));
-        warning "Recovering after Isar toplevel crash -- see also Isar.crashes");
-      raw_loop secure src)
+    handle exn =>
+      (Output.error_msg (Toplevel.exn_message exn)
+        handle crash =>
+          (CRITICAL (fn () => change crashes (cons crash));
+            warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
+          raw_loop secure src)
   end;
 
 in
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/isar_cmd.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Derived Isar commands.
@@ -219,7 +218,7 @@
 (* goals *)
 
 fun goal opt_chain goal stmt int =
-  opt_chain #> goal NONE (K Seq.single) stmt int;
+  opt_chain #> goal NONE (K I) stmt int;
 
 val have = goal I Proof.have;
 val hence = goal Proof.chain Proof.have;
@@ -229,12 +228,12 @@
 
 (* local endings *)
 
-fun local_qed m = Toplevel.proofs (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proofs o Proof.local_terminal_proof;
-val local_default_proof = Toplevel.proofs Proof.local_default_proof;
-val local_immediate_proof = Toplevel.proofs Proof.local_immediate_proof;
-val local_done_proof = Toplevel.proofs Proof.local_done_proof;
-val local_skip_proof = Toplevel.proofs' Proof.local_skip_proof;
+fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
+val local_terminal_proof = Toplevel.proof o Proof.local_terminal_proof;
+val local_default_proof = Toplevel.proof Proof.local_default_proof;
+val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
+val local_done_proof = Toplevel.proof Proof.local_done_proof;
+val local_skip_proof = Toplevel.proof' Proof.local_skip_proof;
 
 val skip_local_qed = Toplevel.skip_proof (fn i => if i > 1 then i - 1 else raise Toplevel.UNDEF);
 
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -393,7 +393,7 @@
     (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Expression.add_locale_cmd name name expr elems #> snd)));
+            (Expression.add_locale_cmd name "" expr elems #> snd)));
 
 val _ =
   OuterSyntax.command "sublocale"
@@ -470,7 +470,7 @@
    (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
     >> (fn ((name, (supclasses, elems)), begin) =>
         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-          (Class.class_cmd name supclasses elems #-> TheoryTarget.begin)));
+          (Class.class_cmd name supclasses elems #> snd)));
 
 val _ =
   OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/locale.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -31,7 +31,6 @@
 sig
   type locale
 
-  val test_locale: theory -> string -> bool
   val register_locale: bstring ->
     (string * sort) list * (Binding.T * typ option * mixfix) list ->
     term option * term list ->
@@ -44,6 +43,7 @@
   val extern: theory -> string -> xstring
 
   (* Specification *)
+  val defined: theory -> string -> bool
   val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
   val instance_of: theory -> string -> Morphism.morphism -> term list
   val specification_of: theory -> string -> term option * term list
@@ -71,11 +71,11 @@
   val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
 
   (* Registrations *)
-  val add_global_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
+  val add_registration: (string * (Morphism.morphism * Morphism.morphism)) ->
     theory -> theory
-  val amend_global_registration: Morphism.morphism -> (string * Morphism.morphism) ->
+  val amend_registration: Morphism.morphism -> (string * Morphism.morphism) ->
     theory -> theory
-  val get_global_registrations: theory -> (string * Morphism.morphism) list
+  val get_registrations: theory -> (string * Morphism.morphism) list
 
   (* Diagnostic *)
   val print_locales: theory -> unit
@@ -109,107 +109,79 @@
 datatype ctxt = datatype Element.ctxt;
 
 
-(*** Basics ***)
+
+(*** Theory data ***)
 
 datatype locale = Loc of {
-  (* extensible lists are in reverse order: decls, notes, dependencies *)
+  (** static part **)
   parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
     (* type and term parameters *)
   spec: term option * term list,
     (* assumptions (as a single predicate expression) and defines *)
+  (** dynamic part **)
   decls: (declaration * stamp) list * (declaration * stamp) list,
     (* type and term syntax declarations *)
   notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
     (* theorem declarations *)
   dependencies: ((string * Morphism.morphism) * stamp) list
     (* locale dependencies (sublocale relation) *)
-}
+};
 
-
-(*** Theory data ***)
+fun mk_locale ((parameters, spec), ((decls, notes), dependencies)) =
+  Loc {parameters = parameters, spec = spec, decls = decls,
+    notes = notes, dependencies = dependencies};
+fun map_locale f (Loc {parameters, spec, decls, notes, dependencies}) =
+  mk_locale (f ((parameters, spec), ((decls, notes), dependencies)));
+fun merge_locale (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
+  Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
+    mk_locale ((parameters, spec),
+      (((merge (eq_snd op =) (decls1, decls1'), merge (eq_snd op =) (decls2, decls2')),
+        merge (eq_snd op =) (notes, notes')),
+          merge (eq_snd op =) (dependencies, dependencies')));
 
 structure LocalesData = TheoryDataFun
 (
-  type T = NameSpace.T * locale Symtab.table;
-    (* locale namespace and locales of the theory *)
-
+  type T = locale NameSpace.table;
   val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
-
-  fun join_locales _
-   (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
-    Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
-      Loc {
-        parameters = parameters,
-        spec = spec,
-        decls =
-         (merge (eq_snd op =) (decls1, decls1'),
-          merge (eq_snd op =) (decls2, decls2')),
-        notes = merge (eq_snd op =) (notes, notes'),
-        dependencies = merge (eq_snd op =) (dependencies, dependencies')};
-
-  fun merge _ = NameSpace.join_tables join_locales;
+  fun merge _ = NameSpace.join_tables (K merge_locale);
 );
 
 val intern = NameSpace.intern o #1 o LocalesData.get;
 val extern = NameSpace.extern o #1 o LocalesData.get;
 
-fun get_locale thy name = Symtab.lookup (#2 (LocalesData.get thy)) name;
+fun get_locale thy = Symtab.lookup (#2 (LocalesData.get thy));
+
+fun defined thy = is_some o get_locale thy;
 
 fun the_locale thy name = case get_locale thy name
- of SOME loc => loc
+ of SOME (Loc loc) => loc
   | NONE => error ("Unknown locale " ^ quote name);
 
-fun test_locale thy name = case get_locale thy name
- of SOME _ => true | NONE => false;
-
 fun register_locale bname parameters spec decls notes dependencies thy =
   thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
-    Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
-      dependencies = dependencies}) #> snd);
+    mk_locale ((parameters, spec), ((decls, notes), dependencies))) #> snd);
 
-fun change_locale name f thy =
-  let
-    val Loc {parameters, spec, decls, notes, dependencies} =
-        the_locale thy name;
-    val (parameters', spec', decls', notes', dependencies') =
-      f (parameters, spec, decls, notes, dependencies);
-  in
-    thy
-    |> (LocalesData.map o apsnd) (Symtab.update (name, Loc {parameters = parameters',
-      spec = spec', decls = decls', notes = notes', dependencies = dependencies'}))
-  end;
+fun change_locale name =
+  LocalesData.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
 
 fun print_locales thy =
-  let val (space, locs) = LocalesData.get thy in
-    Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
-    |> Pretty.writeln
-  end;
+  Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (LocalesData.get thy)))
+  |> Pretty.writeln;
 
 
 (*** Primitive operations ***)
 
-fun params_of thy name =
-  let
-    val Loc {parameters = (_, params), ...} = the_locale thy name
-  in params end;
+fun params_of thy = snd o #parameters o the_locale thy;
 
-fun instance_of thy name morph =
-  params_of thy name |>
-    map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
+fun instance_of thy name morph = params_of thy name |>
+  map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
 
-fun specification_of thy name =
-  let
-    val Loc {spec, ...} = the_locale thy name
-  in spec end;
+fun specification_of thy = #spec o the_locale thy;
 
-fun declarations_of thy name =
-  let
-    val Loc {decls, ...} = the_locale thy name
-  in
-    decls |> apfst (map fst) |> apsnd (map fst)
-  end;
+fun declarations_of thy name = the_locale thy name |>
+  #decls |> apfst (map fst) |> apsnd (map fst);
 
 
 (*** Activate context elements of locale ***)
@@ -267,7 +239,7 @@
   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   else
     let
-      val Loc {parameters = (_, params), dependencies, ...} = the_locale thy name;
+      val {parameters = (_, params), dependencies, ...} = the_locale thy name;
       val instance = instance_of thy name morph;
     in
       if member (ident_eq thy) marked (name, instance)
@@ -304,7 +276,7 @@
 
 fun activate_decls thy (name, morph) ctxt =
   let
-    val Loc {decls = (typ_decls, term_decls), ...} = the_locale thy name;
+    val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   in
     ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
       fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
@@ -312,7 +284,7 @@
 
 fun activate_notes activ_elem transfer thy (name, morph) input =
   let
-    val Loc {notes, ...} = the_locale thy name;
+    val {notes, ...} = the_locale thy name;
     fun activate ((kind, facts), _) input =
       let
         val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph))
@@ -323,7 +295,7 @@
 
 fun activate_all name thy activ_elem transfer (marked, input) =
   let
-    val Loc {parameters = (_, params), spec = (asm, defs), ...} =
+    val {parameters = (_, params), spec = (asm, defs), ...} =
       the_locale thy name;
   in
     input |>
@@ -342,9 +314,9 @@
 local
 
 fun init_global_elem (Notes (kind, facts)) thy =
-      let
-        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
-      in Old_Locale.global_note_qualified kind facts' thy |> snd end
+  let
+    val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
+  in Old_Locale.global_note_qualified kind facts' thy |> snd end
 
 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
       ProofContext.add_fixes_i fixes |> snd
@@ -408,42 +380,40 @@
 
 (*** Registrations: interpretations in theories ***)
 
-(* FIXME only global variant needed *)
-structure RegistrationsData = GenericDataFun
+structure RegistrationsData = TheoryDataFun
 (
   type T = ((string * (Morphism.morphism * Morphism.morphism)) * stamp) list;
-(* FIXME mixins need to be stamped *)
+    (* FIXME mixins need to be stamped *)
     (* registrations, in reverse order of declaration *)
   val empty = [];
   val extend = I;
+  val copy = I;
   fun merge _ data : T = Library.merge (eq_snd op =) data;
     (* FIXME consolidate with dependencies, consider one data slot only *)
 );
 
-val get_global_registrations =
-  Context.Theory #> RegistrationsData.get #> map fst #> map (apsnd op $>);
+val get_registrations =
+  RegistrationsData.get #> map fst #> map (apsnd op $>);
 
-fun add_global reg =
-  (Context.theory_map o RegistrationsData.map) (cons (reg, stamp ()));
-
-fun add_global_registration (name, (base_morph, export)) thy =
-  roundup thy (fn _ => fn (name', morph') => fn thy => add_global (name', (morph', export)) thy)
+fun add_registration (name, (base_morph, export)) thy =
+  roundup thy (fn _ => fn (name', morph') =>
+    (RegistrationsData.map o cons) ((name', (morph', export)), stamp ()))
     (name, base_morph) (get_global_idents thy, thy) |>
     snd (* FIXME ?? uncurry put_global_idents *);
 
-fun amend_global_registration morph (name, base_morph) thy =
+fun amend_registration morph (name, base_morph) thy =
   let
-    val regs = (Context.Theory #> RegistrationsData.get #> map fst) thy;
+    val regs = (RegistrationsData.get #> map fst) thy;
     val base = instance_of thy name base_morph;
     fun match (name', (morph', _)) =
       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
     val i = find_index match (rev regs);
-    val _ = if i = ~1 then error ("No interpretation of locale " ^
+    val _ = if i = ~1 then error ("No registration of locale " ^
         quote (extern thy name) ^ " and parameter instantiation " ^
         space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
       else ();
   in
-    (Context.theory_map o RegistrationsData.map) (nth_map (length regs - 1 - i)
+    RegistrationsData.map (nth_map (length regs - 1 - i)
       (fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
   end;
 
@@ -456,16 +426,15 @@
   let
     val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
     val ctxt'' = ctxt' |> ProofContext.theory (
-      change_locale loc
-        (fn (parameters, spec, decls, notes, dependencies) =>
-          (parameters, spec, decls, (args', stamp ()) :: notes, dependencies)) #>
+      (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
+        #>
       (* Registrations *)
       (fn thy => fold_rev (fn (name, morph) =>
             let
               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
                 Attrib.map_facts (Attrib.attribute_i thy)
             in Old_Locale.global_note_qualified kind args'' #> snd end)
-        (get_global_registrations thy |> filter (fn (name, _) => name = loc)) thy))
+        (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   in ctxt'' end;
 
 
@@ -476,9 +445,8 @@
 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
 
 fun add_decls add loc decl =
-  ProofContext.theory (change_locale loc
-    (fn (parameters, spec, decls, notes, dependencies) =>
-      (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
+  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
+    #>
   add_thmss loc Thm.internalK
     [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
 
@@ -492,10 +460,7 @@
 
 (* Dependencies *)
 
-fun add_dependency loc dep =
-  change_locale loc
-    (fn (parameters, spec, decls, notes, dependencies) =>
-      (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies));
+fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
 
 
 (*** Reasoning about locales ***)
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/obtain.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/obtain.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 The 'obtain' and 'guess' language elements -- generalized existence at
@@ -150,13 +149,13 @@
 
     fun after_qed _ =
       Proof.local_qed (NONE, false)
-      #> Seq.map (`Proof.the_fact #-> (fn rule =>
+      #> `Proof.the_fact #-> (fn rule =>
         Proof.fix_i vars
-        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms));
+        #> Proof.assm_i (obtain_export fix_ctxt rule (map (cert o Free) parms)) asms);
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K Seq.single) [((Binding.empty, []), [(obtain_prop, [])])] int
+    |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume_i
@@ -306,7 +305,7 @@
     val before_qed = SOME (Method.primitive_text (Goal.conclude #> MetaSimplifier.norm_hhf #>
         (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th))));
     fun after_qed [[_, res]] =
-      Proof.end_block #> guess_context (check_result ctxt thesis res) #> Seq.single;
+      Proof.end_block #> guess_context (check_result ctxt thesis res);
   in
     state
     |> Proof.enter_forward
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/old_locale.ML
--- a/src/Pure/Isar/old_locale.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/old_locale.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -116,7 +116,7 @@
     theory -> Proof.state
   val interpretation_in_locale: (Proof.context -> Proof.context) ->
     xstring * expr -> theory -> Proof.state
-  val interpret: (Proof.state -> Proof.state Seq.seq) ->
+  val interpret: (Proof.state -> Proof.state) ->
     (Binding.T -> Binding.T) -> expr ->
     term option list * (Attrib.binding * term) list ->
     bool -> Proof.state ->
@@ -2478,7 +2478,7 @@
 
 val interpret = gen_interpret prep_local_registration;
 fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
-  Seq.single (standard_name_morph interp_prfx);
+  I (standard_name_morph interp_prfx);
 
 end;
 
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -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 97916a925a69 -r 85bc8b63747c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/proof.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -30,7 +30,6 @@
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
   val get_goal: state -> context * (thm list * thm)
-  val schematic_goal: state -> bool
   val show_main_goal: bool ref
   val verbose: bool ref
   val pretty_state: int -> state -> Pretty.T list
@@ -87,35 +86,40 @@
   val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
     (theory -> 'a -> attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
-    string -> Method.text option -> (thm list list -> state -> state Seq.seq) ->
+    string -> Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * 'a list) * 'b) list -> state -> state
-  val local_qed: Method.text option * bool -> state -> state Seq.seq
+  val local_qed: Method.text option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
   val theorem_i: Method.text option -> (thm list list -> context -> context) ->
     (term * term list) list list -> context -> state
   val global_qed: Method.text option * bool -> state -> context
-  val local_terminal_proof: Method.text * Method.text option -> state -> state Seq.seq
-  val local_default_proof: state -> state Seq.seq
-  val local_immediate_proof: state -> state Seq.seq
-  val local_done_proof: state -> state Seq.seq
-  val local_skip_proof: bool -> state -> state Seq.seq
+  val local_terminal_proof: Method.text * Method.text option -> state -> state
+  val local_default_proof: state -> state
+  val local_immediate_proof: state -> state
+  val local_skip_proof: bool -> state -> state
+  val local_done_proof: state -> state
   val global_terminal_proof: Method.text * Method.text option -> state -> context
   val global_default_proof: state -> context
   val global_immediate_proof: state -> context
+  val global_skip_proof: bool -> state -> context
   val global_done_proof: state -> context
-  val global_skip_proof: bool -> state -> context
-  val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val have: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val have_i: Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
-  val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val show: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
-  val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
+  val show_i: Method.text option -> (thm list list -> state -> state) ->
     ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+  val schematic_goal: state -> bool
   val is_relevant: state -> bool
-  val future_proof: (state -> ('a * context) future) -> state -> 'a future * context
-  val future_terminal_proof: Method.text * Method.text option -> state -> context
+  val local_future_proof: (state -> ('a * state) Future.future) ->
+    state -> 'a Future.future * state
+  val global_future_proof: (state -> ('a * Proof.context) Future.future) ->
+    state -> 'a Future.future * context
+  val local_future_terminal_proof: Method.text * Method.text option -> bool -> state -> state
+  val global_future_terminal_proof: Method.text * Method.text option -> bool -> state -> context
 end;
 
 structure Proof: PROOF =
@@ -148,7 +152,7 @@
     goal: thm,                            (*subgoals ==> statement*)
     before_qed: Method.text option,
     after_qed:
-      (thm list list -> state -> state Seq.seq) *
+      (thm list list -> state -> state) *
       (thm list list -> context -> context)};
 
 fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
@@ -312,12 +316,6 @@
   let val (ctxt, (_, {using, goal, ...})) = find_goal state
   in (ctxt, (using, goal)) end;
 
-fun schematic_goal state =
-  let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state in
-    Term.exists_subterm Term.is_Var prop orelse
-    Term.exists_type (Term.exists_subtype Term.is_TVar) prop
-  end;
-
 
 
 (** pretty_state **)
@@ -347,8 +345,7 @@
       (case filter_out (fn s => s = "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i,
-            {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
+    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
           [Pretty.str ("goal" ^
@@ -751,6 +748,13 @@
   |> `before_qed |-> (refine o the_default Method.succeed_text)
   |> Seq.maps (refine (Method.finish_text txt (Position.thread_data ())));
 
+fun check_result msg sq =
+  (case Seq.pull sq of
+    NONE => error msg
+  | SOME (s, _) => s);
+
+fun check_finish sq = check_result "Failed to finish proof" sq;
+
 
 (* unstructured refinement *)
 
@@ -842,7 +846,7 @@
       |> burrow (ProofContext.export goal_ctxt outer_ctxt);
 
     val (after_local, after_global) = after_qed;
-    fun after_local' x y = Position.setmp_thread_data_seq pos (fn () => after_local x y) ();
+    fun after_local' x y = Position.setmp_thread_data pos (fn () => after_local x y) ();
     fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
   in
     outer_state
@@ -871,61 +875,47 @@
     |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
   end;
 
-fun local_qed txt =
-  end_proof false txt #>
-  Seq.maps (generic_qed ProofContext.auto_bind_facts #->
+fun local_qeds txt =
+  end_proof false txt
+  #> Seq.map (generic_qed ProofContext.auto_bind_facts #->
     (fn ((after_qed, _), results) => after_qed results));
 
+fun local_qed txt = local_qeds txt #> check_finish;
+
 
 (* global goals *)
 
 fun global_goal prepp before_qed after_qed propp ctxt =
   init ctxt
-  |> generic_goal (prepp #> ProofContext.auto_fixes) ""
-    before_qed (K Seq.single, after_qed) propp;
+  |> generic_goal (prepp #> ProofContext.auto_fixes) "" before_qed (K I, after_qed) propp;
 
 val theorem = global_goal ProofContext.bind_propp_schematic;
 val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
 
-fun check_result msg sq =
-  (case Seq.pull sq of
-    NONE => error msg
-  | SOME (s', sq') => Seq.cons s' sq');
-
 fun global_qeds txt =
   end_proof true txt
   #> Seq.map (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
-    after_qed results (context_of state)))
-  |> Seq.DETERM;   (*backtracking may destroy theory!*)
+    after_qed results (context_of state)));
 
-fun global_qed txt =
-  global_qeds txt
-  #> check_result "Failed to finish proof"
-  #> Seq.hd;
+fun global_qed txt = global_qeds txt #> check_finish;
 
 
 (* concluding steps *)
 
-fun local_terminal_proof (text, opt_text) =
-  proof (SOME text) #> Seq.maps (local_qed (opt_text, true));
+fun terminal_proof qed initial terminal =
+  proof (SOME initial) #> Seq.maps (qed terminal) #> check_finish;
 
+fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
 val local_default_proof = local_terminal_proof (Method.default_text, NONE);
 val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
-val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false));
 fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE);
+val local_done_proof = terminal_proof local_qeds Method.done_text (NONE, false);
 
-fun global_term_proof immed (text, opt_text) =
-  proof (SOME text)
-  #> check_result "Terminal proof method failed"
-  #> Seq.maps (global_qeds (opt_text, immed))
-  #> check_result "Failed to finish proof (after successful terminal method)"
-  #> Seq.hd;
-
-val global_terminal_proof = global_term_proof true;
+fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
 val global_default_proof = global_terminal_proof (Method.default_text, NONE);
 val global_immediate_proof = global_terminal_proof (Method.this_text, NONE);
-val global_done_proof = global_term_proof false (Method.done_text, NONE);
 fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
+val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
 
 
 (* common goal statements *)
@@ -940,7 +930,7 @@
     val testing = ref false;
     val rule = ref (NONE: thm option);
     fun fail_msg ctxt =
-      "Local statement will fail to solve any pending goal" ::
+      "Local statement will fail to refine any pending goal" ::
       (case ! rule of NONE => [] | SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th])
       |> cat_lines;
 
@@ -951,13 +941,14 @@
       else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th)
       else ();
     val test_proof =
-      (Seq.pull oo local_skip_proof) true
+      try (local_skip_proof true)
       |> setmp_noncritical testing true
       |> Exn.capture;
 
     fun after_qed' results =
       refine_goals print_rule (context_of state) (flat results)
-      #> Seq.maps (after_qed results);
+      #> check_result "Failed to refine any pending goal"
+      #> after_qed results;
   in
     state
     |> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
@@ -979,59 +970,89 @@
 end;
 
 
-(* fork global proofs *)
+
+(** future proofs **)
+
+(* relevant proof states *)
+
+fun is_schematic t =
+  Term.exists_subterm Term.is_Var t orelse
+  Term.exists_type (Term.exists_subtype Term.is_TVar) t;
+
+fun schematic_goal state =
+  let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state
+  in is_schematic prop end;
+
+fun is_relevant state =
+  (case try find_goal state of
+    NONE => true
+  | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
+      is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
+
+
+(* full proofs *)
 
 local
 
-fun is_original state =
-  (case try find_goal state of
-    NONE => false
-  | SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
-      Logic.protect prop aconv Thm.concl_of goal);
-
-in
-
-fun is_relevant state =
-  can (assert_bottom false) state orelse
-  can assert_forward state orelse
-  not (is_original state) orelse
-  schematic_goal state;
-
-fun future_proof fork_proof state =
+fun future_proof done get_context fork_proof state =
   let
-    val _ = is_relevant state andalso error "Cannot fork relevant proof";
-
+    val _ = assert_backward state;
     val (goal_ctxt, (_, goal)) = find_goal state;
     val {statement as (kind, propss, prop), messages, using, goal, before_qed, after_qed} = goal;
 
+    val _ = is_relevant state andalso error "Cannot fork relevant proof";
+
     val prop' = Logic.protect prop;
     val statement' = (kind, [[], [prop']], prop');
     val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
       (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
-    fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+
+    fun after_local' [[th]] = put_thms false (AutoBind.thisN, SOME [th]);
+    fun after_global' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
+    val after_qed' = (after_local', after_global');
     val this_name = ProofContext.full_bname goal_ctxt AutoBind.thisN;
 
     val result_ctxt =
       state
-      |> map_contexts (Variable.auto_fixes prop)
-      |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
+      |> map_contexts (Variable.declare_term prop)
+      |> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
       |> fork_proof;
 
-    val future_thm = result_ctxt |> Future.map (fn (_, ctxt) =>
-      ProofContext.get_fact_single ctxt (Facts.named this_name));
-    val finished_goal = Goal.future_result goal_ctxt future_thm prop';
+    val future_thm = result_ctxt |> Future.map (fn (_, x) =>
+      ProofContext.get_fact_single (get_context x) (Facts.named this_name));
+    val finished_goal = exception_trace (fn () => Goal.future_result goal_ctxt future_thm prop');
     val state' =
       state
       |> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed))
-      |> global_done_proof;
+      |> done;
   in (Future.map #1 result_ctxt, state') end;
 
+in
+
+fun local_future_proof x = future_proof local_done_proof context_of x;
+fun global_future_proof x = future_proof global_done_proof I x;
+
 end;
 
-fun future_terminal_proof meths state =
-  if is_relevant state orelse not (Future.enabled ()) then global_terminal_proof meths state
-  else #2 (state |> future_proof (fn state' =>
-    Future.fork_pri ~1 (fn () => ((), global_terminal_proof meths state'))));
+
+(* terminal proofs *)
+
+local
+
+fun future_terminal_proof proof1 proof2 meths int state =
+  if int orelse is_relevant state orelse not (Future.enabled ())
+  then proof1 meths state
+  else snd (state |> proof2 (fn state' => Future.fork_pri ~1 (fn () => ((), proof1 meths state'))));
+
+in
+
+fun local_future_terminal_proof x =
+  future_terminal_proof local_terminal_proof local_future_proof x;
+
+fun global_future_terminal_proof x =
+  future_terminal_proof global_terminal_proof global_future_proof x;
 
 end;
 
+end;
+
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/theory_target.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -334,7 +334,7 @@
 
 fun init_target _ NONE = global_target
   | init_target thy (SOME target) =
-      make_target target (Locale.test_locale thy (Locale.intern thy target))
+      make_target target (Locale.defined thy (Locale.intern thy target))
       true (Class_Target.is_class thy target) ([], [], []) [];
 
 fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
@@ -384,7 +384,7 @@
 
 fun context "-" thy = init NONE thy
   | context target thy = init (SOME (locale_intern
-      (Locale.test_locale thy (Locale.intern thy target)) thy target)) thy;
+      (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
 fun instantiation_cmd raw_arities thy =
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Isar/toplevel.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -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;
 
@@ -716,7 +718,7 @@
         val (body_trs, end_tr) = split_last proof_trs;
         val finish = Context.Theory o ProofContext.theory_of;
 
-        val future_proof = Proof.future_proof
+        val future_proof = Proof.global_future_proof
           (fn prf =>
             Future.fork_pri ~1 (fn () =>
               let val (states, State (result_node, _)) =
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/Tools/invoke.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -88,7 +88,7 @@
           |> (snd o ProofContext.note_thmss_i "" notes)
           |> ProofContext.restore_naming ctxt
         end) #>
-      Proof.put_facts NONE #> Seq.single;
+      Proof.put_facts NONE;
   in
     state'
     |> Proof.chain_facts chain_facts
diff -r 97916a925a69 -r 85bc8b63747c src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Jan 08 12:25:22 2009 -0800
+++ b/src/Pure/context.ML	Thu Jan 08 21:13:40 2009 -0800
@@ -132,7 +132,15 @@
 
 val copy_data = Datatab.map' invoke_copy;
 val extend_data = Datatab.map' invoke_extend;
-fun merge_data pp = Datatab.join (invoke_merge pp) o pairself extend_data;
+
+fun merge_data pp (data1, data2) =
+  Datatab.keys (Datatab.merge (K true) (data1, data2))
+  |> Par_List.map (fn k =>
+    (case (Datatab.lookup data1 k, Datatab.lookup data2 k) of
+      (SOME x, NONE) => (k, invoke_extend k x)
+    | (NONE, SOME y) => (k, invoke_extend k y)
+    | (SOME x, SOME y) => (k, invoke_merge pp k (invoke_extend k x, invoke_extend k y))))
+  |> Datatab.make;
 
 end;