src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36063 cdc6855a6387
parent 36062 194cb6e3c13f
child 36167 c1a35be8e476
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 15:50:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Mar 29 18:44:24 2010 +0200
     1.3 @@ -80,6 +80,8 @@
     1.4  structure Sledgehammer_FOL_Clause : SLEDGEHAMMER_FOL_CLAUSE =
     1.5  struct
     1.6  
     1.7 +open Sledgehammer_Util
     1.8 +
     1.9  val schematic_var_prefix = "V_";
    1.10  val fixed_var_prefix = "v_";
    1.11  
    1.12 @@ -184,8 +186,7 @@
    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 +  if dfg andalso size s > 60 then Word.toString (hashw_string (s, 0w0)) else s;
    1.19  
    1.20  fun lookup_const dfg c =
    1.21      case Symtab.lookup const_trans_table c of