src/HOL/Tools/inductive_set_package.ML
changeset 26336 a0e2b706ce73
parent 26128 fe2d24c26e0c
child 26475 3cc1e48d0ce1
--- a/src/HOL/Tools/inductive_set_package.ML	Wed Mar 19 18:15:25 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Wed Mar 19 22:27:57 2008 +0100
@@ -18,7 +18,7 @@
       local_theory -> InductivePackage.inductive_result * local_theory
   val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
     (string * string option * mixfix) list ->
-    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
+    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     local_theory -> InductivePackage.inductive_result * local_theory
   val setup: theory -> theory
 end;