src/HOL/Nominal/nominal_package.ML
changeset 19275 3d10de7a8ca7
parent 19251 6bc0dda66f32
child 19322 bf84bdf05f14
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed Mar 15 16:18:12 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed Mar 15 17:59:33 2006 +0100
     1.3 @@ -411,7 +411,7 @@
     1.4            (fn _ => EVERY [indtac induction perm_indnames 1,
     1.5               ALLGOALS (asm_full_simp_tac simps)])))
     1.6        in
     1.7 -        foldl (fn ((s, tvs), thy) => AxClass.add_inst_arity_i
     1.8 +        foldl (fn ((s, tvs), thy) => AxClass.prove_arity
     1.9              (s, replicate (length tvs) (cp_class :: classes), [cp_class])
    1.10              (ClassPackage.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
    1.11            thy (full_new_type_names' ~~ tyvars)
    1.12 @@ -420,7 +420,7 @@
    1.13      val (perm_thmss,thy3) = thy2 |>
    1.14        fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
    1.15        curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
    1.16 -        AxClass.add_inst_arity_i (tyname, replicate (length args) classes, classes)
    1.17 +        AxClass.prove_arity (tyname, replicate (length args) classes, classes)
    1.18          (ClassPackage.intro_classes_tac [] THEN REPEAT (EVERY
    1.19             [resolve_tac perm_empty_thms 1,
    1.20              resolve_tac perm_append_thms 1,
    1.21 @@ -585,7 +585,7 @@
    1.22      fun pt_instance ((class, atom), perm_closed_thms) =
    1.23        fold (fn (((({Abs_inverse, Rep_inverse, Rep, ...},
    1.24          perm_def), name), tvs), perm_closed) => fn thy =>
    1.25 -          AxClass.add_inst_arity_i
    1.26 +          AxClass.prove_arity
    1.27              (Sign.intern_type thy name,
    1.28                replicate (length tvs) (classes @ cp_classes), [class])
    1.29              (EVERY [ClassPackage.intro_classes_tac [],
    1.30 @@ -609,7 +609,7 @@
    1.31          val cp1' = PureThy.get_thm thy (Name (name ^ "_inst")) RS cp1
    1.32        in fold (fn ((((({Abs_inverse, Rep_inverse, Rep, ...},
    1.33          perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
    1.34 -          AxClass.add_inst_arity_i
    1.35 +          AxClass.prove_arity
    1.36              (Sign.intern_type thy name,
    1.37                replicate (length tvs) (classes @ cp_classes), [class])
    1.38              (EVERY [ClassPackage.intro_classes_tac [],
    1.39 @@ -1086,7 +1086,7 @@
    1.40        DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
    1.41        fold (fn (atom, ths) => fn thy =>
    1.42          let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
    1.43 -        in fold (fn T => AxClass.add_inst_arity_i
    1.44 +        in fold (fn T => AxClass.prove_arity
    1.45              (fst (dest_Type T),
    1.46                replicate (length sorts) [class], [class])
    1.47              (ClassPackage.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy