1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Jul 23 15:32:30 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Jul 23 15:32:30 2012 +0200
     1.3 @@ -88,11 +88,13 @@
     1.4    val isabelle_info : string -> int -> (string, 'a) ho_term list
     1.5    val extract_isabelle_status : (string, 'a) ho_term list -> string option
     1.6    val extract_isabelle_rank : (string, 'a) ho_term list -> int
     1.7 +  val inductionN : string
     1.8    val introN : string
     1.9    val inductiveN : string
    1.10    val elimN : string
    1.11    val simpN : string
    1.12 -  val defN : string
    1.13 +  val non_rec_defN : string
    1.14 +  val rec_defN : string
    1.15    val rankN : string
    1.16    val minimum_rank : int
    1.17    val default_rank : int
    1.18 @@ -222,11 +224,14 @@
    1.19  
    1.20  val isabelle_info_prefix = "isabelle_"
    1.21  
    1.22 +val inductionN = "induction"
    1.23  val introN = "intro"
    1.24  val inductiveN = "inductive"
    1.25  val elimN = "elim"
    1.26  val simpN = "simp"
    1.27 -val defN = "def"
    1.28 +val non_rec_defN = "non_rec_def"
    1.29 +val rec_defN = "rec_def"
    1.30 +
    1.31  val rankN = "rank"
    1.32  
    1.33  val minimum_rank = 0
    1.34 @@ -503,9 +508,13 @@
    1.35      fun suffix_tag top_level s =
    1.36        if top_level then
    1.37          case extract_isabelle_status info of
    1.38 -          SOME s' => if s' = defN then s ^ ":lt"
    1.39 -                     else if s' = simpN andalso gen_simp then s ^ ":lr"
    1.40 -                     else s
    1.41 +          SOME s' =>
    1.42 +          if s' = non_rec_defN then
    1.43 +            s ^ ":lt"
    1.44 +          else if (s' = simpN orelse s' = rec_defN) andalso gen_simp then
    1.45 +            s ^ ":lr"
    1.46 +          else
    1.47 +            s
    1.48          | NONE => s
    1.49        else
    1.50          s