changeset 46445 | ef9d534e9119 |
parent 46443 | c86276014571 |
child 46643 | a88bccd2b567 |
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 09 14:35:27 2012 +0100 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 09 14:42:18 2012 +0100 @@ -320,7 +320,7 @@ | flatten_type _ = raise Fail "unexpected higher-order type in first-order format" -val dfg_individual_type = "ii" (* cannot clash *) +val dfg_individual_type = "iii" (* cannot clash *) fun str_for_type format ty = let