src/HOL/Nominal/nominal_package.ML
changeset 18366 78b4f225b640
parent 18350 66cda85ea3ab
child 18381 246807ef6dfb
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Dec 07 16:47:04 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Dec 08 10:17:21 2005 +0100
     1.3 @@ -489,8 +489,8 @@
     1.4  
     1.5      val _ = warning "defining type...";
     1.6  
     1.7 -    val (thy6, typedefs) =
     1.8 -      foldl_map (fn (thy, ((((name, mx), tvs), c), name')) =>
     1.9 +    val (typedefs, thy6) =
    1.10 +      fold_map (fn ((((name, mx), tvs), c), name') => fn thy =>
    1.11          setmp TypedefPackage.quiet_mode true
    1.12            (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
    1.13              (rtac exI 1 THEN
    1.14 @@ -502,7 +502,7 @@
    1.15            val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
    1.16            val T = Type (Sign.intern_type thy name, tvs');
    1.17            val Const (_, Type (_, [U])) = c
    1.18 -        in apsnd (pair r o hd)
    1.19 +        in apfst (pair r o hd)
    1.20            (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
    1.21              (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
    1.22               Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
    1.23 @@ -510,8 +510,8 @@
    1.24                   (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
    1.25                     Free ("x", T))))), [])] thy)
    1.26          end))
    1.27 -          (thy5, types_syntax ~~ tyvars ~~
    1.28 -            (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
    1.29 +          (types_syntax ~~ tyvars ~~
    1.30 +            (List.take (ind_consts, length new_type_names)) ~~ new_type_names) thy5;
    1.31  
    1.32      val perm_defs = map snd typedefs;
    1.33      val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
    1.34 @@ -667,7 +667,7 @@
    1.35          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.36            (Const (rep_name, T --> T') $ lhs, rhs));
    1.37          val def_name = (Sign.base_name cname) ^ "_def";
    1.38 -        val (thy', [def_thm]) = thy |>
    1.39 +        val ([def_thm], thy') = thy |>
    1.40            Theory.add_consts_i [(cname', constrT, mx)] |>
    1.41            (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
    1.42        in (thy', defs @ [def_thm], eqns @ [eqn]) end;