# HG changeset patch
# User wenzelm
# Date 1361306677 -3600
# Node ID c3e99efacb673e048feb4c94c97fa3ca53d0dad0
# Parent  c6a8a05ff0a0594ed7dc0aea922652357aa05d7a
back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;

diff -r c6a8a05ff0a0 -r c3e99efacb67 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Feb 19 20:19:21 2013 +0100
+++ b/src/Pure/Pure.thy	Tue Feb 19 21:44:37 2013 +0100
@@ -41,8 +41,8 @@
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" :: thy_decl
-  and "sublocale" "interpretation" :: thy_schematic_goal
-  and "interpret" :: prf_goal % "proof"  (* FIXME schematic? *)
+  and "sublocale" "interpretation" :: thy_goal
+  and "interpret" :: prf_goal % "proof"
   and "class" :: thy_decl
   and "subclass" :: thy_goal
   and "instantiation" :: thy_decl