Fixed bug in subst causing primrec functions returning functions
authorberghofe
Fri May 18 11:12:03 2007 +0200 (2007-05-18)
changeset 23006c46abff9a7a0
parent 23005 914a1de067b6
child 23007 e025695d9b0e
Fixed bug in subst causing primrec functions returning functions
to be rejected.
src/HOL/Nominal/nominal_primrec.ML
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri May 18 09:16:57 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri May 18 11:12:03 2007 +0200
     1.3 @@ -116,11 +116,14 @@
     1.4                  val (x', rs) = (hd rest, tl rest)
     1.5                    handle Empty => raise RecError ("not enough arguments\
     1.6                     \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
     1.7 -                val _ = (case eqns of
     1.8 +                val rs' = (case eqns of
     1.9                      (_, (ls', _, rs', _, _)) :: _ =>
    1.10 -                      if ls = map Free ls' andalso rs = map Free rs' then ()
    1.11 -                      else raise RecError param_err
    1.12 -                  | _ => ());
    1.13 +                      let val (rs1, rs2) = chop (length rs') rs
    1.14 +                      in
    1.15 +                        if ls = map Free ls' andalso rs1 = map Free rs' then rs2
    1.16 +                        else raise RecError param_err
    1.17 +                      end
    1.18 +                  | _ => raise RecError ("no equations for " ^ quote fname'));
    1.19                  val (x, xs) = strip_comb x'
    1.20                in case AList.lookup (op =) subs x
    1.21                 of NONE =>
    1.22 @@ -129,7 +132,7 @@
    1.23                      |-> (fn ts' => pair (list_comb (f, ts')))
    1.24                  | SOME (i', y) =>
    1.25                      fs
    1.26 -                    |> fold_map (subst subs) xs
    1.27 +                    |> fold_map (subst subs) (xs @ rs')
    1.28                      ||> process_fun thy descr rec_eqns (i', fnameT')
    1.29                      |-> (fn ts' => pair (list_comb (y, ts')))
    1.30                end