src/HOL/Nominal/nominal_package.ML
changeset 20483 04aa552a83bc
parent 20411 dd8a1cda2eaf
child 20548 8ef25fe585a8
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Tue Sep 05 22:06:18 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Sep 06 10:01:04 2006 +0200
     1.3 @@ -548,19 +548,20 @@
     1.4  
     1.5      (* FIXME: theorems are stored in database for testing only *)
     1.6      val perm_closed_thmss = map mk_perm_closed atoms;
     1.7 -    val (_,thy5) = PureThy.add_thmss [(("perm_closed", List.concat perm_closed_thmss), [])] thy4;
     1.8 +    val (_, thy5) = PureThy.add_thmss [(("perm_closed", List.concat perm_closed_thmss), [])] thy4;
     1.9  
    1.10      (**** typedef ****)
    1.11  
    1.12      val _ = warning "defining type...";
    1.13  
    1.14      val (typedefs, thy6) =
    1.15 -      fold_map (fn ((((name, mx), tvs), c), name') => fn thy =>
    1.16 +      thy5
    1.17 +      |> fold_map (fn ((((name, mx), tvs), c), name') => fn thy =>
    1.18          setmp TypedefPackage.quiet_mode true
    1.19            (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
    1.20              (rtac exI 1 THEN
    1.21                QUIET_BREADTH_FIRST (has_fewer_prems 1)
    1.22 -              (resolve_tac rep_intrs 1))) thy |> (fn (r, thy) =>
    1.23 +              (resolve_tac rep_intrs 1))) thy |> (fn ((_, r), thy) =>
    1.24          let
    1.25            val permT = mk_permT (TFree (Name.variant tvs "'a", HOLogic.typeS));
    1.26            val pi = Free ("pi", permT);
    1.27 @@ -576,7 +577,7 @@
    1.28                     Free ("x", T))))), [])] thy)
    1.29          end))
    1.30            (types_syntax ~~ tyvars ~~
    1.31 -            (List.take (ind_consts, length new_type_names)) ~~ new_type_names) thy5;
    1.32 +            (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
    1.33  
    1.34      val perm_defs = map snd typedefs;
    1.35      val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;