--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Sep 29 10:39:39 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Sep 29 10:39:39 2014 +0200
@@ -104,6 +104,7 @@
val mk_aconns :
atp_connective -> ('a, 'b, 'c, 'd) atp_formula list
-> ('a, 'b, 'c, 'd) atp_formula
+ val unmangled_type : string -> (string, 'a) ATP_Problem.atp_term
val unmangled_const : string -> string * (string, 'b) atp_term list
val unmangled_const_name : string -> string list
val helper_table : ((string * bool) * (status * thm) list) list