src/HOL/Tools/typedef_package.ML
changeset 25513 b7de6e23e143
parent 25495 98f3596bec44
child 25535 4975b7529a14
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Fri Nov 30 20:13:06 2007 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Fri Nov 30 20:13:07 2007 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4      * (string * string) option -> theory -> Proof.state
     1.5    val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
     1.6      * (string * string) option -> theory -> Proof.state
     1.7 +  val interpretation: (string -> theory -> theory) -> theory -> theory
     1.8  end;
     1.9  
    1.10  structure TypedefPackage: TYPEDEF_PACKAGE =
    1.11 @@ -214,6 +215,9 @@
    1.12  
    1.13  (* add_typedef interfaces *)
    1.14  
    1.15 +structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
    1.16 +val interpretation = TypedefInterpretation.interpretation;
    1.17 +
    1.18  local
    1.19  
    1.20  fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
    1.21 @@ -225,7 +229,11 @@
    1.22      val _ = message ("Proving non-emptiness of set " ^ quote (string_of_term set) ^ " ...");
    1.23      val non_empty = Goal.prove_global thy [] [] goal (K tac) handle ERROR msg =>
    1.24        cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_term set));
    1.25 -  in typedef_result non_empty thy end;
    1.26 +  in
    1.27 +    thy
    1.28 +    |> typedef_result non_empty
    1.29 +    |-> (fn (a, info) => TypedefInterpretation.data a #> pair (a, info))
    1.30 +  end;
    1.31  
    1.32  in
    1.33