# HG changeset patch
# User wenzelm
# Date 1266262256 -3600
# Node ID d8d6c2f55c0c1297921b08bf73358a6c627a4cd4
# Parent  a68e4972fd31142eb734778e505e489849e6ac07
Typedef.the_info;

diff -r a68e4972fd31 -r d8d6c2f55c0c src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Mon Feb 15 20:01:07 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Mon Feb 15 20:30:56 2010 +0100
@@ -19,6 +19,7 @@
   val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
     * (binding * binding) option -> theory -> Proof.state
   val get_info: theory -> string -> info option
+  val the_info: theory -> string -> info
   val interpretation: (string -> theory -> theory) -> theory -> theory
   val setup: theory -> theory
 end;
@@ -45,6 +46,12 @@
 );
 
 val get_info = Symtab.lookup o TypedefData.get;
+
+fun the_info thy name =
+  (case get_info thy name of
+    SOME info => info
+  | NONE => error ("Unknown typedef " ^ quote name));
+
 fun put_info name info = TypedefData.map (Symtab.update (name, info));