1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 01 14:17:02 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 01 15:53:37 2011 +0200
     1.3 @@ -172,6 +172,7 @@
     1.4    if method = e_autoN then
     1.5      "-xAutoDev"
     1.6    else
     1.7 +    (* supplied by Stephan Schulz *)
     1.8      "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \
     1.9      \--destructive-er-aggressive --destructive-er --presat-simplify \
    1.10      \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 14:17:02 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:37 2011 +0200
     2.3 @@ -269,24 +269,19 @@
     2.4      SOME c' => c'
     2.5    | NONE => ascii_of c
     2.6  
     2.7 -(*Remove the initial ' character from a type variable, if it is present*)
     2.8 -fun trim_type_var s =
     2.9 -  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
    2.10 -  else raise Fail ("trim_type: Malformed type variable encountered: " ^ s)
    2.11 -
    2.12 -fun ascii_of_indexname (v,0) = ascii_of v
    2.13 -  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ string_of_int i
    2.14 +fun ascii_of_indexname (v, 0) = ascii_of v
    2.15 +  | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
    2.16  
    2.17  fun make_bound_var x = bound_var_prefix ^ ascii_of x
    2.18  fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
    2.19  fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
    2.20  
    2.21 -fun make_schematic_type_var (x,i) =
    2.22 -      tvar_prefix ^ (ascii_of_indexname (trim_type_var x, i))
    2.23 -fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x))
    2.24 +fun make_schematic_type_var (x, i) =
    2.25 +      tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
    2.26 +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
    2.27  
    2.28 -(* HOL.eq MUST BE "equal" because it's built into ATPs. *)
    2.29 -fun make_fixed_const @{const_name HOL.eq} = "equal"
    2.30 +(* "HOL.eq" is mapped to the ATP's equality. *)
    2.31 +fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal
    2.32    | make_fixed_const c = const_prefix ^ lookup_const c
    2.33  
    2.34  fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
    2.35 @@ -390,8 +385,8 @@
    2.36    | multi_arity_clause ((tcons, ars) :: tc_arlists) =
    2.37        arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
    2.38  
    2.39 -(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
    2.40 -  provided its arguments have the corresponding sorts.*)
    2.41 +(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
    2.42 +   theory thy provided its arguments have the corresponding sorts. *)
    2.43  fun type_class_pairs thy tycons classes =
    2.44    let
    2.45      val alg = Sign.classes_of thy
    2.46 @@ -426,7 +421,8 @@
    2.47     subclass : name,
    2.48     superclass : name}
    2.49  
    2.50 -(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
    2.51 +(* Generate all pairs (sub, super) such that sub is a proper subclass of super
    2.52 +   in theory "thy". *)
    2.53  fun class_pairs _ [] _ = []
    2.54    | class_pairs thy subs supers =
    2.55        let
    2.56 @@ -435,9 +431,8 @@
    2.57          fun add_supers sub = fold (add_super sub) supers
    2.58        in fold add_supers subs [] end
    2.59  
    2.60 -fun make_class_rel_clause (sub,super) =
    2.61 -  {name = sub ^ "_" ^ super,
    2.62 -   subclass = `make_type_class sub,
    2.63 +fun make_class_rel_clause (sub, super) =
    2.64 +  {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
    2.65     superclass = `make_type_class super}
    2.66  
    2.67  fun make_class_rel_clauses thy subs supers =
    2.68 @@ -1367,9 +1362,8 @@
    2.69  val tfree_classes_of_terms = classes_of_terms OldTerm.term_tfrees
    2.70  val tvar_classes_of_terms = classes_of_terms OldTerm.term_tvars
    2.71  
    2.72 -(*fold type constructors*)
    2.73 -fun fold_type_constrs f (Type (a, Ts)) x =
    2.74 -    fold (fold_type_constrs f) Ts (f (a,x))
    2.75 +fun fold_type_constrs f (Type (s, Ts)) x =
    2.76 +    fold (fold_type_constrs f) Ts (f (s, x))
    2.77    | fold_type_constrs _ _ x = x
    2.78  
    2.79  (*Type constructors used to instantiate overloaded constants are the only ones needed.*)