--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 20 10:21:05 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 20 10:45:52 2012 +0100
@@ -466,7 +466,7 @@
fun dfg_string_for_formula gen_simp flavor info =
let
fun suffix_tag top_level s =
- if top_level then
+ if flavor = DFG_Sorted andalso top_level then
case extract_isabelle_status info of
SOME s' => if s' = spec_eqN then s ^ ":lt"
else if s' = simpN andalso gen_simp then s ^ ":lr"
@@ -516,7 +516,11 @@
commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")."
fun formula pred (Formula (ident, kind, phi, _, info)) =
if pred kind then
- let val rank = extract_isabelle_rank info in
+ let
+ val rank =
+ if flavor = DFG_Sorted then extract_isabelle_rank info
+ else default_rank
+ in
"formula(" ^ dfg_string_for_formula gen_simp flavor info phi ^
", " ^ ident ^
(if rank = default_rank then "" else ", " ^ string_of_int rank) ^