diff -r 0016290f904c -r 6a8d18798161 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Tue Jul 10 23:36:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 11 09:32:29 2012 +0200
@@ -14,6 +14,7 @@
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
   val dependencies_of : string list -> thm -> string list
+  val goal_of_thm : thm -> thm
   val meng_paulson_facts :
     Proof.context -> string -> int -> real * real -> thm -> int
     -> (((unit -> string) * stature) * thm) list