# HG changeset patch
# User haftmann
# Date 1123575794 -7200
# Node ID 6dbd7c63a5a653defafcc2d894a627e9ee0b0433
# Parent  bd15f69bd947c319b297bb1d02afda3f07628c9e
exported dest_def

diff -r bd15f69bd947 -r 6dbd7c63a5a6 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Aug 09 10:03:30 2005 +0200
+++ b/src/Pure/theory.ML	Tue Aug 09 10:23:14 2005 +0200
@@ -45,6 +45,7 @@
   val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
   val requires: theory -> string -> string -> unit
   val assert_super: theory -> theory -> theory
+  val dest_def: Pretty.pp -> term -> (string * typ) * term
   val add_axioms: (bstring * string) list -> theory -> theory
   val add_axioms_i: (bstring * term) list -> theory -> theory
   val add_defs: bool -> (bstring * string) list -> theory -> theory