src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 36491 6769f8eacaac
parent 36476 a04cf4704668
child 36493 a3357a631b96
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 28 14:19:26 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Apr 28 15:34:55 2010 +0200
     1.3 @@ -185,7 +185,8 @@
     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 = 63
     1.8 +val max_dfg_symbol_length =
     1.9 +  if is_new_spass_version then 1000000 (* arbitrary large number *) else 63
    1.10  
    1.11  (* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
    1.12  fun controlled_length dfg s =