in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
authorblanchet
Tue Apr 27 14:27:47 2010 +0200 (2010-04-27 ago)
changeset 36476a04cf4704668
parent 36475 05209b869a6b
child 36477 71cc00ea5768
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Apr 27 12:07:07 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Apr 27 14:27:47 2010 +0200
     1.3 @@ -110,20 +110,14 @@
     1.4  (* Provide readable names for the more common symbolic functions *)
     1.5  val const_trans_table =
     1.6    Symtab.make [(@{const_name "op ="}, "equal"),
     1.7 -               (@{const_name Orderings.less_eq}, "lessequals"),
     1.8                 (@{const_name "op &"}, "and"),
     1.9                 (@{const_name "op |"}, "or"),
    1.10                 (@{const_name "op -->"}, "implies"),
    1.11 -               (@{const_name "op :"}, "in"),
    1.12 -               (@{const_name fequal}, "fequal"),
    1.13 -               (@{const_name COMBI}, "COMBI"),
    1.14 -               (@{const_name COMBK}, "COMBK"),
    1.15 -               (@{const_name COMBB}, "COMBB"),
    1.16 -               (@{const_name COMBC}, "COMBC"),
    1.17 -               (@{const_name COMBS}, "COMBS")];
    1.18 +               (@{const_name "op :"}, "in")]
    1.19  
    1.20  val type_const_trans_table =
    1.21 -  Symtab.make [("*", "prod"), ("+", "sum"), ("~=>", "map")];
    1.22 +  Symtab.make [(@{type_name "*"}, "prod"),
    1.23 +               (@{type_name "+"}, "sum")]
    1.24  
    1.25  (*Escaping of special characters.
    1.26    Alphanumeric characters are left unchanged.
    1.27 @@ -263,7 +257,9 @@
    1.28      val s' =
    1.29        if s' = "" orelse not (Char.isAlpha (String.sub (s', 0))) then "X" ^ s'
    1.30        else s'
    1.31 -    val s' = if s' = "op" then full_name else s'
    1.32 +    (* Avoid "equal", since it's built into ATPs; and "op" is very ambiguous
    1.33 +       ("op &", "op |", etc.). *)
    1.34 +    val s' = if s' = "equal" orelse s' = "op" then full_name else s'
    1.35    in
    1.36      case (Char.isLower (String.sub (full_name, 0)),
    1.37            Char.isLower (String.sub (s', 0))) of