back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
authorwenzelm
Tue, 19 Feb 2013 21:44:37 +0100
changeset 51224 c3e99efacb67
parent 51223 c6a8a05ff0a0
child 51225 3fe0d8d55975
back to non-schematic 'sublocale' and 'interpretation' (despite df8fc0567a3d) for more potential parallelism;
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