# HG changeset patch
# User blanchet
# Date 1328019198 -3600
# Node ID b99ca1a7c63ba472e117ce7d344564c7e7e6f6c7
# Parent  ef62c2fafa9e9ecaf7879cbfaf6ac5ebe820c614
avoid name clash, really

diff -r ef62c2fafa9e -r b99ca1a7c63b src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 31 15:10:03 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 31 15:13:18 2012 +0100
@@ -285,7 +285,7 @@
   | flatten_type _ =
     raise Fail "unexpected higher-order type in first-order format"
 
-val dfg_individual_type = "i" (* shouldn't clash *)
+val dfg_individual_type = "ii" (* cannot clash *)
 
 fun str_for_type format ty =
   let