adaption to argument change in primrec_package
authorhaftmann
Fri Jul 21 14:48:17 2006 +0200 (2006-07-21)
changeset 20179a2f3f523c84b
parent 20178 e56fa3c8b1f1
child 20180 a751bec7cf29
adaption to argument change in primrec_package
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Jul 21 14:47:44 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Jul 21 14:48:17 2006 +0200
     1.3 @@ -61,19 +61,19 @@
     1.4      (* <ak>_infinite: infinite (UNIV::<ak_type> set) *)
     1.5      val (inf_axs,thy2) = PureThy.add_axioms_i (map (fn (ak_name, T) =>
     1.6        let 
     1.7 -	val name = ak_name ^ "_infinite"
     1.8 +    val name = ak_name ^ "_infinite"
     1.9          val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not
    1.10                      (HOLogic.mk_mem (HOLogic.mk_UNIV T,
    1.11                       Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))
    1.12        in
    1.13 -	((name, axiom), []) 
    1.14 +        ((name, axiom), []) 
    1.15        end) ak_names_types) thy1;
    1.16      
    1.17      (* declares a swapping function for every atom-kind, it is         *)
    1.18      (* const swap_<ak> :: <akT> * <akT> => <akT> => <akT>              *)
    1.19      (* swap_<ak> (a,b) c = (if a=c then b (else if b=c then a else c)) *)
    1.20      (* overloades then the general swap-function                       *) 
    1.21 -    val (thy3, swap_eqs) = foldl_map (fn (thy, (ak_name, T)) =>
    1.22 +    val (swap_eqs, thy3) = fold_map (fn (ak_name, T) => fn thy =>
    1.23        let
    1.24          val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
    1.25          val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name);
    1.26 @@ -87,21 +87,22 @@
    1.27  
    1.28          val name = "swap_"^ak_name^"_def";
    1.29          val def1 = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.30 -		   (cswap_akname $ HOLogic.mk_prod (a,b) $ c,
    1.31 +                (cswap_akname $ HOLogic.mk_prod (a,b) $ c,
    1.32                      cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
    1.33          val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
    1.34        in
    1.35          thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
    1.36 -            |> (#2 o PureThy.add_defs_unchecked_i true [((name, def2),[])])
    1.37 -            |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]            
    1.38 -      end) (thy2, ak_names_types);
    1.39 +            |> PureThy.add_defs_unchecked_i true [((name, def2),[])]
    1.40 +            |> snd
    1.41 +            |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
    1.42 +      end) ak_names_types thy2;
    1.43      
    1.44      (* declares a permutation function for every atom-kind acting  *)
    1.45      (* on such atoms                                               *)
    1.46      (* const <ak>_prm_<ak> :: (<akT> * <akT>)list => akT => akT    *)
    1.47      (* <ak>_prm_<ak> []     a = a                                  *)
    1.48      (* <ak>_prm_<ak> (x#xs) a = swap_<ak> x (perm xs a)            *)
    1.49 -    val (thy4, prm_eqs) = foldl_map (fn (thy, (ak_name, T)) =>
    1.50 +    val (prm_eqs, thy4) = fold_map (fn (ak_name, T) => fn thy =>
    1.51        let
    1.52          val swapT = HOLogic.mk_prodT (T, T) --> T --> T;
    1.53          val swap_name = Sign.full_name (sign_of thy) ("swap_" ^ ak_name)
    1.54 @@ -122,7 +123,7 @@
    1.55        in
    1.56          thy |> Theory.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
    1.57              |> PrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
    1.58 -      end) (thy3, ak_names_types);
    1.59 +      end) ak_names_types thy3;
    1.60      
    1.61      (* defines permutation functions for all combinations of atom-kinds; *)
    1.62      (* there are a trivial cases and non-trivial cases                   *)
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Jul 21 14:47:44 2006 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Jul 21 14:48:17 2006 +0200
     2.3 @@ -238,7 +238,7 @@
     2.4          end) constrs
     2.5        end) descr);
     2.6  
     2.7 -    val (thy2, perm_simps) = thy1 |>
     2.8 +    val (perm_simps, thy2) = thy1 |>
     2.9        Theory.add_consts_i (map (fn (s, T) => (Sign.base_name s, T, NoSyn))
    2.10          (List.drop (perm_names_types, length new_type_names))) |>
    2.11        PrimrecPackage.add_primrec_unchecked_i "" perm_eqs;