--- a/src/HOL/Tools/typedef_package.ML Tue Jun 30 20:57:46 1998 +0200
+++ b/src/HOL/Tools/typedef_package.ML Wed Jul 01 11:20:32 1998 +0200
@@ -7,6 +7,7 @@
signature TYPEDEF_PACKAGE =
sig
+ val add_typedecls: (bstring * string list * mixfix) list -> theory -> theory
val prove_nonempty: cterm -> thm list -> tactic option -> thm
val add_typedef: string -> bstring * string list * mixfix ->
string -> string list -> thm list -> tactic option -> theory -> theory
@@ -18,6 +19,24 @@
struct
+(** type declarations **)
+
+fun add_typedecls decls thy =
+ let
+ val full = Sign.full_name (Theory.sign_of thy);
+
+ fun arity_of (raw_name, args, mx) =
+ (full (Syntax.type_name raw_name mx), replicate (length args) HOLogic.termS, HOLogic.termS);
+ in
+ thy
+ |> PureThy.add_typedecls decls
+ |> Theory.add_arities_i (map arity_of decls)
+ end;
+
+
+
+(** type definitions **)
+
(* prove non-emptyness of a set *) (*exception ERROR*)
val is_def = Logic.is_equals o #prop o rep_thm;