# HG changeset patch
# User wenzelm
# Date 899284832 -7200
# Node ID 230cca8452c71028dedebed3f1b5f7f5aa861edb
# Parent  866a281a8c2a0f2c041a750a115c66557d39e23f
added add_typedecls;

diff -r 866a281a8c2a -r 230cca8452c7 src/HOL/Tools/typedef_package.ML
--- 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;