# HG changeset patch
# User haftmann
# Date 1196449987 -3600
# Node ID b7de6e23e143bb93657da5f71da56da804e0b296
# Parent  4134f7c782e2029b2c3322c9bcf36b0d11443de3
interpretation for typedefs

diff -r 4134f7c782e2 -r b7de6e23e143 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Fri Nov 30 20:13:06 2007 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Fri Nov 30 20:13:07 2007 +0100
@@ -23,6 +23,7 @@
     * (string * string) option -> theory -> Proof.state
   val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     * (string * string) option -> theory -> Proof.state
+  val interpretation: (string -> theory -> theory) -> theory -> theory
 end;
 
 structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -214,6 +215,9 @@
 
 (* add_typedef interfaces *)
 
+structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
+val interpretation = TypedefInterpretation.interpretation;
+
 local
 
 fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
@@ -225,7 +229,11 @@
     val _ = message ("Proving non-emptiness of set " ^ quote (string_of_term set) ^ " ...");
     val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
       cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_term set));
-  in typedef_result non_empty thy end;
+  in
+    thy
+    |> typedef_result non_empty
+    |-> (fn (a, info) => TypedefInterpretation.data a #> pair (a, info))
+  end;
 
 in