--- a/src/HOL/Import/proof_kernel.ML Wed Oct 22 14:15:43 2008 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Oct 22 14:15:44 2008 +0200
@@ -2097,7 +2097,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 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
@@ -2183,7 +2183,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 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/Import/replay.ML Wed Oct 22 14:15:43 2008 +0200
+++ b/src/HOL/Import/replay.ML Wed Oct 22 14:15:44 2008 +0200
@@ -344,7 +344,7 @@
| delta (Hol_theorem (thyname, thmname, th)) thy =
add_hol4_theorem thyname thmname ([], th_of thy th) thy
| delta (Typedef (thmname, typ, c, repabs, th)) thy =
- snd (TypedefPackage.add_typedef_i false thmname typ c repabs (rtac (th_of thy th) 1) thy)
+ snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy)
| delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =
add_hol4_type_mapping thyname tycname true fulltyname thy
| delta (Indexed_theorem (i, th)) thy =
--- a/src/HOL/Nominal/nominal_package.ML Wed Oct 22 14:15:43 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Wed Oct 22 14:15:44 2008 +0200
@@ -608,7 +608,7 @@
val (typedefs, thy6) =
thy4
|> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
- TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx)
+ TypedefPackage.add_typedef false (SOME name') (name, tvs, mx)
(Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
Const (cname, U --> HOLogic.boolT)) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Oct 22 14:15:43 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Oct 22 14:15:44 2008 +0200
@@ -194,7 +194,7 @@
val (typedefs, thy3) = thy2 |>
parent_path flat_names |>
fold_map (fn ((((name, mx), tvs), c), name') =>
- TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx)
+ TypedefPackage.add_typedef false (SOME name') (name, tvs, mx)
(Collect $ Const (c, UnivT')) NONE
(rtac exI 1 THEN rtac CollectI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
--- a/src/HOL/Tools/typedef_package.ML Wed Oct 22 14:15:43 2008 +0200
+++ b/src/HOL/Tools/typedef_package.ML Wed Oct 22 14:15:44 2008 +0200
@@ -15,12 +15,10 @@
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 -> (string * info) * theory
- val add_typedef_i: bool -> string option -> bstring * string list * mixfix ->
term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
- val typedef: (bool * string) * (bstring * string list * mixfix) * string
+ val typedef: (bool * string) * (bstring * string list * mixfix) * term
* (string * string) option -> theory -> Proof.state
- val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
+ val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string
* (string * string) option -> theory -> Proof.state
val interpretation: (string -> theory -> theory) -> theory -> theory
val setup: theory -> theory
@@ -33,15 +31,15 @@
val type_definitionN = "Typedef.type_definition";
-val Rep = thm "type_definition.Rep";
-val Rep_inverse = thm "type_definition.Rep_inverse";
-val Abs_inverse = thm "type_definition.Abs_inverse";
-val Rep_inject = thm "type_definition.Rep_inject";
-val Abs_inject = thm "type_definition.Abs_inject";
-val Rep_cases = thm "type_definition.Rep_cases";
-val Abs_cases = thm "type_definition.Abs_cases";
-val Rep_induct = thm "type_definition.Rep_induct";
-val Abs_induct = thm "type_definition.Abs_induct";
+val Rep = @{thm "type_definition.Rep"};
+val Rep_inverse = @{thm "type_definition.Rep_inverse"};
+val Abs_inverse = @{thm "type_definition.Abs_inverse"};
+val Rep_inject = @{thm "type_definition.Rep_inject"};
+val Abs_inject = @{thm "type_definition.Abs_inject"};
+val Rep_cases = @{thm "type_definition.Rep_cases"};
+val Abs_cases = @{thm "type_definition.Abs_cases"};
+val Rep_induct = @{thm "type_definition.Rep_induct"};
+val Abs_induct = @{thm "type_definition.Abs_induct"};
@@ -214,27 +212,18 @@
handle ERROR msg => err_in_typedef msg name;
-(* add_typedef interfaces *)
+(* add_typedef interface *)
-local
-
-fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
+fun add_typedef def opt_name typ set opt_morphs tac thy =
let
val name = the_default (#1 typ) opt_name;
val (set, goal, _, typedef_result) =
- prepare_typedef prep_term def name typ set opt_morphs thy;
+ prepare_typedef Syntax.check_term def name typ set opt_morphs thy;
val non_empty = Goal.prove_global thy [] [] goal (K tac)
handle ERROR msg => cat_error msg
("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
in typedef_result non_empty thy end;
-in
-
-val add_typedef = gen_typedef Syntax.read_term;
-val add_typedef_i = gen_typedef Syntax.check_term;
-
-end;
-
(* Isar typedef interface *)
@@ -249,8 +238,8 @@
in
-val typedef = gen_typedef Syntax.read_term;
-val typedef_i = gen_typedef Syntax.check_term;
+val typedef = gen_typedef Syntax.check_term;
+val typedef_cmd = gen_typedef Syntax.read_term;
end;
@@ -270,7 +259,7 @@
Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
- typedef ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
+ typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
val _ =
OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
--- a/src/HOLCF/Tools/pcpodef_package.ML Wed Oct 22 14:15:43 2008 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Wed Oct 22 14:15:44 2008 +0200
@@ -89,7 +89,7 @@
fun make_po tac thy1 =
let
val ((_, {type_definition, set_def, ...}), thy2) = thy1
- |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac;
+ |> TypedefPackage.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
val lthy3 = thy2
|> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
val less_def' = Syntax.check_term lthy3 less_def;