# HG changeset patch
# User wenzelm
# Date 1213901281 -7200
# Node ID 7b7ce2d7fafe49d4d0581c3a9a9051d791f246c0
# Parent  ea82bd1e3c2009f8577c3c1da48f6908f4496a17
export read_typ/cert_typ -- version with regular context operations;

diff -r ea82bd1e3c20 -r 7b7ce2d7fafe src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Jun 19 20:48:00 2008 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Jun 19 20:48:01 2008 +0200
@@ -24,6 +24,8 @@
   val make_case :  Proof.context -> bool -> string list -> term ->
     (term * term) list -> term * (term * (int * bool)) list
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
+  val read_typ: theory ->
+    (typ list * (string * sort) list) * string -> typ list * (string * sort) list
   val interpretation : (string list -> theory -> theory) -> theory -> theory
   val rep_datatype : ({distinct : thm list list,
        inject : thm list list,
@@ -304,17 +306,18 @@
 
 (* prepare types *)
 
-fun read_typ sign ((Ts, sorts), str) =
+fun read_typ thy ((Ts, sorts), str) =
   let
-    val T = Type.no_tvars (Sign.read_def_typ (sign, AList.lookup (op =)
-      (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
-  in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
+    val ctxt = ProofContext.init thy
+      |> fold (Variable.declare_typ o TFree) sorts;
+    val T = Syntax.read_typ ctxt str;
+  in (Ts @ [T], Term.add_tfreesT T sorts) end;
 
 fun cert_typ sign ((Ts, sorts), raw_T) =
   let
     val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
       TYPE (msg, _, _) => error msg;
-    val sorts' = add_typ_tfrees (T, sorts)
+    val sorts' = Term.add_tfreesT T sorts;
   in (Ts @ [T],
       case duplicates (op =) (map fst sorts') of
          [] => sorts'