src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 37414 d0cea0796295
parent 36966 adc11fb3f3aa
child 37479 f6b1ee5b420b
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Jun 14 16:17:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Mon Jun 14 16:43:44 2010 +0200
     1.3 @@ -193,8 +193,7 @@
     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 -val max_dfg_symbol_length =
     1.8 -  if is_new_spass_version then 1000000 (* arbitrary large number *) else 63
     1.9 +val max_dfg_symbol_length = 63
    1.10  
    1.11  (* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
    1.12  fun controlled_length dfg s =