# HG changeset patch # User huffman # Date 1215181988 -7200 # Node ID c61507a98bff3f3c39bb57693becc18e78ffcf81 # Parent a5de2cbf548ff03b84cef514141aa44028681502 prefer theorem names without numbers diff -r a5de2cbf548f -r c61507a98bff src/Pure/Isar/find_theorems.ML --- a/src/Pure/Isar/find_theorems.ML Fri Jul 04 15:57:55 2008 +0200 +++ b/src/Pure/Isar/find_theorems.ML Fri Jul 04 16:33:08 2008 +0200 @@ -234,16 +234,20 @@ local +val index_ord = option_ord (K EQUAL); val hidden_ord = bool_ord o pairself NameSpace.is_hidden; val qual_ord = int_ord o pairself (length o NameSpace.explode); val txt_ord = int_ord o pairself size; -fun nicer_name x y = - (case hidden_ord (x, y) of - EQUAL => (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) +fun nicer_name (x, i) (y, j) = + (case hidden_ord (x, y) of EQUAL => + (case index_ord (i, j) of EQUAL => + (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) + | ord => ord) | ord => ord) <> GREATER; -fun nicer (Facts.Named ((x, _), _)) (Facts.Named ((y, _), _)) = nicer_name x y +fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = + nicer_name (x, i) (y, j) | nicer (Facts.Fact _) (Facts.Named _) = true | nicer (Facts.Named _) (Facts.Fact _) = false;