src/HOL/Tools/BNF/bnf_lfp_compat.ML
changeset 58684 56b9eab818ca
parent 58665 50b229a5a097
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Oct 14 19:39:29 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Oct 15 17:15:11 2014 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    val datatype_compat_cmd: string list -> local_theory -> local_theory
     1.5    val add_datatype: preference list -> Old_Datatype_Aux.spec list -> theory -> string list * theory
     1.6    val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
     1.7 -   local_theory -> (term list * thm list) * local_theory
     1.8 +    local_theory -> (term list * thm list) * local_theory
     1.9    val add_primrec_global: (binding * typ option * mixfix) list ->
    1.10      (Attrib.binding * term) list -> theory -> (term list * thm list) * theory
    1.11    val add_primrec_overloaded: (string * (string * typ) * bool) list ->