src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36062 194cb6e3c13f
parent 35865 2f8fb5242799
child 36063 cdc6855a6387
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 15:26:19 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 15:50:18 2010 +0200
     1.3 @@ -180,11 +180,11 @@
     1.4        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
     1.5  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
     1.6  
     1.7 -(*HACK because SPASS truncates identifiers to 63 characters :-(( *)
     1.8 -(*32-bit hash,so we expect no collisions unless there are around 65536 long identifiers...*)
     1.9 -fun controlled_length dfg_format s =
    1.10 -  if size s > 60 andalso dfg_format
    1.11 -  then Word.toString (Polyhash.hashw_string(s,0w0))
    1.12 +(* HACK because SPASS 3.0 truncates identifiers to 63 characters. (This is
    1.13 +   solved in 3.7 and perhaps in earlier versions too.) *)
    1.14 +(* 32-bit hash, so we expect no collisions. *)
    1.15 +fun controlled_length dfg s =
    1.16 +  if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0))
    1.17    else s;
    1.18  
    1.19  fun lookup_const dfg c =
    1.20 @@ -197,8 +197,9 @@
    1.21          SOME c' => c'
    1.22        | NONE => controlled_length dfg (ascii_of c);
    1.23  
    1.24 -fun make_fixed_const _ "op =" = "equal"   (*MUST BE "equal" because it's built-in to ATPs*)
    1.25 -  | make_fixed_const dfg c      = const_prefix ^ lookup_const dfg c;
    1.26 +(* "op =" MUST BE "equal" because it's built into ATPs. *)
    1.27 +fun make_fixed_const _ (@{const_name "op ="}) = "equal"
    1.28 +  | make_fixed_const dfg c = const_prefix ^ lookup_const dfg c;
    1.29  
    1.30  fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c;
    1.31