src/HOL/Tools/datatype_realizer.ML
changeset 13641 63d1790a43ed
parent 13467 d66b526192bf
child 13656 58bb243dbafb
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Oct 10 14:23:47 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Oct 10 14:26:50 2002 +0200
     1.3 @@ -88,23 +88,18 @@
     1.4                  in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
     1.5                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
     1.6                  end
     1.7 -            | mk_prems vs (((DtRec k, s), T) :: ds) = 
     1.8 +            | mk_prems vs (((dt, s), T) :: ds) = 
     1.9                  let
    1.10 +                  val k = body_index dt;
    1.11 +                  val (Us, U) = strip_type T;
    1.12 +                  val i = length Us;
    1.13                    val rT = nth_elem (k, rec_result_Ts);
    1.14 -                  val r = Free ("r" ^ s, rT);
    1.15 +                  val r = Free ("r" ^ s, Us ---> rT);
    1.16                    val (p, f) = mk_prems (vs @ [r]) ds
    1.17 -                in (mk_all k ("r" ^ s) rT (Logic.mk_implies
    1.18 -                  (HOLogic.mk_Trueprop (make_pred k rT T r (Free (s, T))), p)), f)
    1.19 -                end
    1.20 -            | mk_prems vs (((DtType ("fun", [_, DtRec k]), s),
    1.21 -                  T' as Type ("fun", [T, U])) :: ds) =
    1.22 -                let
    1.23 -                  val rT = nth_elem (k, rec_result_Ts);
    1.24 -                  val r = Free ("r" ^ s, T --> rT);
    1.25 -                  val (p, f) = mk_prems (vs @ [r]) ds
    1.26 -                in (mk_all k ("r" ^ s) (T --> rT) (Logic.mk_implies
    1.27 -                  (all T $ Abs ("x", T, HOLogic.mk_Trueprop (make_pred k rT U
    1.28 -                    (r $ Bound 0) (Free (s, T') $ Bound 0))), p)), f)
    1.29 +                in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
    1.30 +                  (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
    1.31 +                    (make_pred k rT U (app_bnds r i)
    1.32 +                      (app_bnds (Free (s, T)) i))), p)), f)
    1.33                  end
    1.34  
    1.35          in (j + 1,