# HG changeset patch # User blanchet # Date 1323941930 -3600 # Node ID bfb5234a70bac352c5bd84530bda5ffd3f7727f6 # Parent 728cc85534713f4a1d4dace8eda73e810e014ebe made SML/NJ happier diff -r 728cc8553471 -r bfb5234a70ba src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Dec 15 09:13:32 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Thu Dec 15 10:38:50 2011 +0100 @@ -75,10 +75,11 @@ open ATP_Proof open ATP_Translate -structure String_Redirect = - ATP_Redirect(type key = step_name - val ord = fast_string_ord o pairself fst - val string_of = fst) +structure String_Redirect = ATP_Redirect( + type key = step_name + val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') + val string_of = fst) + open String_Redirect datatype reconstructor =