diff -r 961bbcc9d85b -r a0e2b706ce73 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -43,10 +43,11 @@
     local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
-  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list
-    -> local_theory -> (bstring * thm list) list * local_theory
-  val theorems_cmd: string -> ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list
-    -> local_theory -> (bstring * thm list) list * local_theory
+  val theorems: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list ->
+    local_theory -> (bstring * thm list) list * local_theory
+  val theorems_cmd: string ->
+    ((bstring * Attrib.src list) * (Facts.ref * Attrib.src list) list) list ->
+    local_theory -> (bstring * thm list) list * local_theory
   val theorem: string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) ->
     string * Attrib.src list -> Element.context_i Locale.element list -> Element.statement_i ->