1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
     1.3 @@ -482,7 +482,8 @@
     1.4                  case strip_prefix_and_unascii schematic_var_prefix a of
     1.5                    SOME b => Var ((b, var_index), T)
     1.6                  | NONE =>
     1.7 -                  Var ((repair_variable_name Char.toLower a, var_index), T)
     1.8 +                  Var ((a |> textual ? repair_variable_name Char.toLower,
     1.9 +                        var_index), T)
    1.10            in list_comb (t, ts) end
    1.11    in do_term [] end
    1.12  
    1.13 @@ -547,7 +548,7 @@
    1.14          #>> quantify_over_var (case q of
    1.15                                   AForall => forall_of
    1.16                                 | AExists => exists_of)
    1.17 -                              (repair_variable_name Char.toLower s)
    1.18 +                              (s |> textual ? repair_variable_name Char.toLower)
    1.19        | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
    1.20        | AConn (c, [phi1, phi2]) =>
    1.21          do_formula (pos |> c = AImplies ? not) phi1