src/Pure/Pure.thy
changeset 51274 cfc83ad52571
parent 51270 17d30843fc3b
child 51293 05b1bbae748d
--- a/src/Pure/Pure.thy	Mon Feb 25 12:52:27 2013 +0100
+++ b/src/Pure/Pure.thy	Mon Feb 25 13:29:19 2013 +0100
@@ -50,7 +50,7 @@
   and "overloading" :: thy_decl
   and "code_datatype" :: thy_decl
   and "theorem" "lemma" "corollary" :: thy_goal
-  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
+  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_goal
   and "notepad" :: thy_decl
   and "have" :: prf_goal % "proof"
   and "hence" :: prf_goal % "proof" == "then have"