1.1 --- a/src/HOL/Tools/typedef.ML	Mon Feb 15 20:01:07 2010 +0100
     1.2 +++ b/src/HOL/Tools/typedef.ML	Mon Feb 15 20:30:56 2010 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4    val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
     1.5      * (binding * binding) option -> theory -> Proof.state
     1.6    val get_info: theory -> string -> info option
     1.7 +  val the_info: theory -> string -> info
     1.8    val interpretation: (string -> theory -> theory) -> theory -> theory
     1.9    val setup: theory -> theory
    1.10  end;
    1.11 @@ -45,6 +46,12 @@
    1.12  );
    1.13  
    1.14  val get_info = Symtab.lookup o TypedefData.get;
    1.15 +
    1.16 +fun the_info thy name =
    1.17 +  (case get_info thy name of
    1.18 +    SOME info => info
    1.19 +  | NONE => error ("Unknown typedef " ^ quote name));
    1.20 +
    1.21  fun put_info name info = TypedefData.map (Symtab.update (name, info));
    1.22  
    1.23