| changeset 70586 | 57df8a85317a |
| parent 70569 | 095dadc62bb5 |
| child 70587 | 729f4d066d1a |
--- a/src/Pure/thm.ML Tue Aug 20 09:48:22 2019 +0200 +++ b/src/Pure/thm.ML Tue Aug 20 11:01:05 2019 +0200 @@ -371,7 +371,7 @@ local -val constraint_ord : constraint * constraint -> order = +val constraint_ord : constraint ord = Context.theory_id_ord o apply2 (Context.theory_id o #theory) <<< Term_Ord.typ_ord o apply2 #typ <<< Term_Ord.sort_ord o apply2 #sort;