--- a/src/HOL/Import/proof_kernel.ML Tue Sep 05 22:06:18 2006 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Sep 06 10:01:04 2006 +0200
@@ -2094,7 +2094,7 @@
val tnames = map fst tfrees
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
- val (typedef_info, thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
+ val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false (SOME thmname) typ c NONE (rtac th2 1) thy
val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
val th3 = (#type_definition typedef_info) RS typedef_hol2hol4
@@ -2187,7 +2187,7 @@
val tnames = sort string_ord (map fst tfrees)
val tsyn = mk_syn thy tycname
val typ = (tycname,tnames,tsyn)
- val (typedef_info, thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
+ val ((_, typedef_info), thy') = TypedefPackage.add_typedef_i false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy
val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
val fulltyname = Sign.intern_type thy' tycname
val aty = Type (fulltyname, map mk_vartype tnames)
--- a/src/HOL/Nominal/nominal_package.ML Tue Sep 05 22:06:18 2006 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Wed Sep 06 10:01:04 2006 +0200
@@ -548,19 +548,20 @@
(* FIXME: theorems are stored in database for testing only *)
val perm_closed_thmss = map mk_perm_closed atoms;
- val (_,thy5) = PureThy.add_thmss [(("perm_closed", List.concat perm_closed_thmss), [])] thy4;
+ val (_, thy5) = PureThy.add_thmss [(("perm_closed", List.concat perm_closed_thmss), [])] thy4;
(**** typedef ****)
val _ = warning "defining type...";
val (typedefs, thy6) =
- fold_map (fn ((((name, mx), tvs), c), name') => fn thy =>
+ thy5
+ |> fold_map (fn ((((name, mx), tvs), c), name') => fn thy =>
setmp TypedefPackage.quiet_mode true
(TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
(rtac exI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
- (resolve_tac rep_intrs 1))) thy |> (fn (r, thy) =>
+ (resolve_tac rep_intrs 1))) thy |> (fn ((_, r), thy) =>
let
val permT = mk_permT (TFree (Name.variant tvs "'a", HOLogic.typeS));
val pi = Free ("pi", permT);
@@ -576,7 +577,7 @@
Free ("x", T))))), [])] thy)
end))
(types_syntax ~~ tyvars ~~
- (List.take (ind_consts, length new_type_names)) ~~ new_type_names) thy5;
+ (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
val perm_defs = map snd typedefs;
val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
--- a/src/HOL/Tools/typecopy_package.ML Tue Sep 05 22:06:18 2006 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Wed Sep 06 10:01:04 2006 +0200
@@ -16,7 +16,7 @@
proj_def: thm
}
val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
- -> theory -> info * theory
+ -> theory -> (string * info) * theory
val get_typecopies: theory -> string list
val get_typecopy_info: theory -> string -> info option
type hook = string * info -> theory -> theory;
@@ -94,16 +94,15 @@
local
-fun gen_add_typecopy prep_typ (tyco, raw_vs) raw_ty constr_proj thy =
+fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy =
let
val ty = prep_typ thy raw_ty;
val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
val tac = Tactic.rtac UNIV_witness 1;
- fun add_info ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
+ fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
Rep_name = c_rep, Abs_inject = inject,
Abs_inverse = inverse, ... } : TypedefPackage.info ) thy =
let
- val Type (tyco', _) = ty_abs;
val exists_thm =
UNIV_I
|> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
@@ -119,15 +118,16 @@
};
in
thy
- |> (TypecopyData.map o apfst o Symtab.update_new) (tyco', info)
- |> invoke_hooks (tyco', info)
- |> pair info
+ |> (TypecopyData.map o apfst o Symtab.update_new) (tyco, info)
+ |> invoke_hooks (tyco, info)
+ |> pair (tyco, info)
end
in
thy
- |> TypedefPackage.add_typedef_i false (SOME tyco) (tyco, map fst vs, NoSyn)
- (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
- |-> (fn info => add_info info)
+ |> setmp TypedefPackage.quiet_mode true
+ (TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
+ (HOLogic.mk_UNIV ty) (Option.map swap constr_proj)) tac
+ |-> (fn (tyco, info) => add_info tyco info)
end;
in
--- a/src/HOL/Tools/typedef_package.ML Tue Sep 05 22:06:18 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML Wed Sep 06 10:01:04 2006 +0200
@@ -16,9 +16,9 @@
Abs_cases: thm, Rep_induct: thm, Abs_induct: thm};
val get_info: theory -> string -> info option
val add_typedef: bool -> string option -> bstring * string list * mixfix ->
- string -> (bstring * bstring) option -> tactic -> theory -> info * theory
+ string -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
val add_typedef_i: bool -> string option -> bstring * string list * mixfix ->
- term -> (bstring * bstring) option -> tactic -> theory -> info * theory
+ term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
val typedef: (bool * string) * (bstring * string list * mixfix) * string
* (string * string) option -> theory -> Proof.state
val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
@@ -197,7 +197,7 @@
Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
val thy3 = thy2 |> put_info full_tname info;
- in (info, Context.Theory thy3) end);
+ in ((full_tname, info), Context.Theory thy3) end);
(* errors *)
@@ -268,9 +268,12 @@
val (_, goal, goal_pat, typedef_result) =
prepare_typedef prep_term def name typ set opt_morphs thy;
fun att (thy, th) =
- let val ({type_definition, ...}, thy') = typedef_result th thy
+ let val ((name, {type_definition, ...}), thy') = typedef_result th thy
in (thy', type_definition) end;
- in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, [goal_pat]) thy end;
+ in
+ thy
+ |> IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, [goal_pat])
+ end;
in
--- a/src/HOLCF/pcpodef_package.ML Tue Sep 05 22:06:18 2006 +0200
+++ b/src/HOLCF/pcpodef_package.ML Wed Sep 06 10:01:04 2006 +0200
@@ -101,7 +101,7 @@
||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
(ClassPackage.intro_classes_tac [])
||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
- |-> (fn ({type_definition, set_def, ...}, [less_definition]) =>
+ |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) =>
AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
(Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
#> rpair (type_definition, less_definition, set_def));