# HG changeset patch
# User blanchet
# Date 1332236752 -3600
# Node ID d810a9130d55738c5ae2e3d6d32ff884ec58a383
# Parent  78e88d26f19de64536be47e52a42de9391fa50d9
don't generate new SPASS constructs for old SPASS

diff -r 78e88d26f19d -r d810a9130d55 src/HOL/Tools/ATP/atp_problem.ML
--- 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) ^