--- 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