src/HOL/Nominal/nominal_package.ML
changeset 18381 246807ef6dfb
parent 18366 78b4f225b640
child 18579 002d371401f5
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Dec 09 15:25:52 2005 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sat Dec 10 00:11:35 2005 +0100
     1.3 @@ -359,7 +359,7 @@
     1.4            thy (full_new_type_names' ~~ tyvars)
     1.5        end;
     1.6  
     1.7 -    val (thy3, perm_thmss) = thy2 |>
     1.8 +    val (perm_thmss,thy3) = thy2 |>
     1.9        fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
    1.10        curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
    1.11          AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
    1.12 @@ -482,8 +482,7 @@
    1.13  
    1.14      (* FIXME: theorems are stored in database for testing only *)
    1.15      val perm_closed_thmss = map mk_perm_closed atoms;
    1.16 -    val (thy5, _) = PureThy.add_thmss [(("perm_closed",
    1.17 -      List.concat perm_closed_thmss), [])] thy4;
    1.18 +    val (_,thy5) = PureThy.add_thmss [(("perm_closed", List.concat perm_closed_thmss), [])] thy4;
    1.19  
    1.20      (**** typedef ****)
    1.21  
    1.22 @@ -1067,9 +1066,9 @@
    1.23  
    1.24      val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global];
    1.25  
    1.26 -    val (_, thy9) = thy8 |>
    1.27 +    val (_, thy9) = (thy8:Context.theory) |>
    1.28        Theory.add_path big_name |>
    1.29 -      (PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] #> Library.swap) ||>
    1.30 +      PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] ||>
    1.31        Theory.parent_path ||>>
    1.32        DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
    1.33        DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
    1.34 @@ -1085,7 +1084,7 @@
    1.35              (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    1.36          end) (atoms ~~ finite_supp_thms) ||>
    1.37        Theory.add_path big_name ||>>
    1.38 -      (PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] #> Library.swap) ||>
    1.39 +      PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] ||>
    1.40        Theory.parent_path;
    1.41  
    1.42    in