src/HOL/Tools/inductive_package.ML
changeset 26336 a0e2b706ce73
parent 26128 fe2d24c26e0c
child 26477 ecf06644f6cb
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Mar 19 22:27:57 2008 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4        local_theory -> inductive_result * local_theory
     1.5    val add_inductive: bool -> bool -> (string * string option * mixfix) list ->
     1.6      (string * string option * mixfix) list ->
     1.7 -    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
     1.8 +    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
     1.9      local_theory -> inductive_result * local_theory
    1.10    val add_inductive_global: string ->
    1.11      {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} ->
    1.12 @@ -76,7 +76,7 @@
    1.13    val gen_add_inductive: add_ind_def ->
    1.14      bool -> bool -> (string * string option * mixfix) list ->
    1.15      (string * string option * mixfix) list ->
    1.16 -    ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list ->
    1.17 +    ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list ->
    1.18      local_theory -> inductive_result * local_theory
    1.19    val gen_ind_decl: add_ind_def ->
    1.20      bool -> OuterParse.token list ->