# HG changeset patch
# User wenzelm
# Date 1196264805 -3600
# Node ID f781564f3605e42b475a07ad42b49c71ac34b91f
# Parent  1c9b3733f887f84f818cb8fe1bbe19680ca584c0
removed (cf. object_logic.ML);

diff -r 1c9b3733f887 -r f781564f3605 src/Pure/typedecl.ML
--- a/src/Pure/typedecl.ML	Wed Nov 28 16:44:24 2007 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/typedecl.ML
-    ID:         $Id$
-    Author:     Florian Haftmann, TU Muenchen
-
-Type declarations with interpretation.
-*)
-
-signature TYPEDECL =
-sig
-  val add: bstring * string list * mixfix -> theory -> typ * theory
-  val interpretation: (string -> theory -> theory) -> theory -> theory
-end
-
-structure Typedecl: TYPEDECL =
-struct
-
-structure TypedeclInterpretation = InterpretationFun(type T = string val eq = op =);
-val interpretation = TypedeclInterpretation.interpretation;
-
-val _ = Context.add_setup TypedeclInterpretation.init;
-
-fun add (a, vs, mx) thy =
-  let
-    val _ = has_duplicates (op =) vs andalso
-      error ("Duplicate parameters in type declaration: " ^ quote a);
-    val a' = Sign.full_name thy a;
-    val T = Type (a', map (fn v => TFree (v, [])) vs);
-  in
-    thy
-    |> Sign.add_types [(a, length vs, mx)]
-    |> TypedeclInterpretation.data a'
-    |> pair T
-  end;
-
-end;