more error checking for fixrec
authorhuffman
Thu Dec 08 13:25:54 2011 +0100 (2011-12-08)
changeset 457879fcaf2557c59
parent 45786 3f07a7a91180
child 45788 9049b24959de
more error checking for fixrec
src/HOL/HOLCF/Tools/fixrec.ML
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Thu Dec 08 13:25:40 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Thu Dec 08 13:25:54 2011 +0100
     1.3 @@ -270,6 +270,7 @@
     1.4      val const =
     1.5          case distinct (op =) consts of
     1.6            [n] => n
     1.7 +        | [] => fixrec_err "no defining equations for function"
     1.8          | _ => fixrec_err "all equations in block must define the same function"
     1.9      val vars =
    1.10          case distinct (op = o pairself length) (map fst matchers) of
    1.11 @@ -337,12 +338,15 @@
    1.12      val (fixes : ((binding * typ) * mixfix) list,
    1.13           spec : (Attrib.binding * term) list) =
    1.14            fst (prep_spec raw_fixes raw_spec lthy)
    1.15 +    val names = map (Binding.name_of o fst o fst) fixes
    1.16 +    fun check_head name =
    1.17 +        member (op =) names name orelse
    1.18 +        fixrec_err ("Illegal equation head. Expected " ^ commas_quote names)
    1.19      val chead_of_spec =
    1.20        chead_of o fst o dest_eqs o Logic.strip_imp_concl o strip_alls o snd
    1.21 -    fun name_of (Free (n, _)) = n
    1.22 +    fun name_of (Free (n, _)) = tap check_head n
    1.23        | name_of _ = fixrec_err ("unknown term")
    1.24      val all_names = map (name_of o chead_of_spec) spec
    1.25 -    val names = distinct (op =) all_names
    1.26      fun block_of_name n =
    1.27        map_filter
    1.28          (fn (m,eq) => if m = n then SOME eq else NONE)