# HG changeset patch
# User wenzelm
# Date 1192213317 -7200
# Node ID 633afd909ff29b8b89785d7f4f56d5f94aee6052
# Parent  8bc74ba1423d46f654bebe4613467829d23881ca
more informative TheoryTarget.peek operation;

diff -r 8bc74ba1423d -r 633afd909ff2 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Oct 12 20:21:56 2007 +0200
+++ b/src/Pure/Isar/specification.ML	Fri Oct 12 20:21:57 2007 +0200
@@ -299,8 +299,9 @@
 
     val (loc, ctxt, lthy) =
       (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
-        (SOME loc, true) => (* workaround non-modularity of in/includes *)  (* FIXME *)
-          (SOME loc, ProofContext.init thy, LocalTheory.restore lthy0)
+        ({target, is_locale = true, ...}, true) =>
+          (*temporary workaround for non-modularity of in/includes*)  (* FIXME *)
+          (SOME target, ProofContext.init thy, LocalTheory.restore lthy0)
       | _ => (NONE, lthy0, lthy0));
 
     val attrib = prep_att thy;
diff -r 8bc74ba1423d -r 633afd909ff2 src/Pure/Isar/subclass.ML
--- a/src/Pure/Isar/subclass.ML	Fri Oct 12 20:21:56 2007 +0200
+++ b/src/Pure/Isar/subclass.ML	Fri Oct 12 20:21:57 2007 +0200
@@ -54,9 +54,9 @@
     val thy = ProofContext.theory_of ctxt;
     val ctxt_thy = ProofContext.init thy;
     val sup = prep_class thy raw_sup;
-    val sub = case Option.mapPartial (Class.class_of_locale thy) (TheoryTarget.peek lthy)
-     of NONE => error "not in class context"
-      | SOME sub => sub;
+    val sub = case TheoryTarget.peek lthy
+     of {is_class = false, ...} => error "No class context"
+      | {target, ...} => target;
     val sub_params = map fst (Class.these_params thy [sub]);
     val sup_params = map fst (Class.these_params thy [sup]);
     val err_params = subtract (op =) sub_params sup_params;