src/HOL/Nominal/nominal_package.ML
changeset 18302 577e5d19b33c
parent 18280 45e139675daf
child 18350 66cda85ea3ab
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Nov 30 15:30:08 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Nov 30 16:59:19 2005 +0100
     1.3 @@ -1024,7 +1024,7 @@
     1.4      val fsT = TFree ("'n", ind_sort);
     1.5  
     1.6      fun make_pred i T =
     1.7 -      Free (List.nth (pnames, i), T --> fsT --> HOLogic.boolT);
     1.8 +      Free (List.nth (pnames, i), fsT --> T --> HOLogic.boolT);
     1.9  
    1.10      fun make_ind_prem k T ((cname, cargs), idxs) =
    1.11        let
    1.12 @@ -1041,7 +1041,7 @@
    1.13              val (Us, U) = strip_type T;
    1.14              val l = length Us
    1.15            in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop
    1.16 -            (make_pred (body_index dt) U $ app_bnds (Free (s, T)) l $ Bound l))
    1.17 +            (make_pred (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l))
    1.18            end;
    1.19  
    1.20          val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
    1.21 @@ -1051,9 +1051,9 @@
    1.22            (map (curry List.nth frees) (List.concat (map (fn (m, n) =>
    1.23               m upto m + n - 1) idxs)))
    1.24  
    1.25 -      in list_all_free (z :: frees, Logic.list_implies (prems' @ prems,
    1.26 -        HOLogic.mk_Trueprop (make_pred k T $ 
    1.27 -          list_comb (Const (cname, Ts ---> T), map Free frees) $ Free z)))
    1.28 +      in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
    1.29 +        HOLogic.mk_Trueprop (make_pred k T $ Free z $
    1.30 +          list_comb (Const (cname, Ts ---> T), map Free frees))))
    1.31        end;
    1.32  
    1.33      val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
    1.34 @@ -1061,7 +1061,7 @@
    1.35      val tnames = DatatypeProp.make_tnames recTs;
    1.36      val z = (variant tnames "z", fsT);
    1.37      val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
    1.38 -      (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T) $ Free z)
    1.39 +      (map (fn (((i, _), T), tname) => make_pred i T $ Free z $ Free (tname, T))
    1.40          (descr'' ~~ recTs ~~ tnames)));
    1.41      val induct = Logic.list_implies (ind_prems, ind_concl);
    1.42