src/Pure/term_ord.ML
changeset 43794 49cbbe2768a8
parent 37852 a902f158b4fc
child 67561 f0b11413f1c9
     1.1 --- a/src/Pure/term_ord.ML	Wed Jul 13 20:13:27 2011 +0200
     1.2 +++ b/src/Pure/term_ord.ML	Wed Jul 13 20:36:18 2011 +0200
     1.3 @@ -19,6 +19,7 @@
     1.4    val sort_ord: sort * sort -> order
     1.5    val typ_ord: typ * typ -> order
     1.6    val fast_term_ord: term * term -> order
     1.7 +  val syntax_term_ord: term * term -> order
     1.8    val indexname_ord: indexname * indexname -> order
     1.9    val tvar_ord: (indexname * sort) * (indexname * sort) -> order
    1.10    val var_ord: (indexname * typ) * (indexname * typ) -> order
    1.11 @@ -84,7 +85,7 @@
    1.12    | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
    1.13    | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
    1.14    | atoms_ord (Bound i, Bound j) = int_ord (i, j)
    1.15 -  | atoms_ord _ = raise Fail "atoms_ord";
    1.16 +  | atoms_ord _ = EQUAL;
    1.17  
    1.18  fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
    1.19        (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
    1.20 @@ -93,8 +94,13 @@
    1.21    | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
    1.22    | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
    1.23    | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
    1.24 -  | types_ord (Bound _, Bound _) = EQUAL
    1.25 -  | types_ord _ = raise Fail "types_ord";
    1.26 +  | types_ord _ = EQUAL;
    1.27 +
    1.28 +fun comments_ord (Abs (x, _, t), Abs (y, _, u)) =
    1.29 +      (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord)
    1.30 +  | comments_ord (t1 $ t2, u1 $ u2) =
    1.31 +      (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord)
    1.32 +  | comments_ord _ = EQUAL;
    1.33  
    1.34  in
    1.35  
    1.36 @@ -105,6 +111,9 @@
    1.37        EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
    1.38      | ord => ord);
    1.39  
    1.40 +fun syntax_term_ord tu =
    1.41 +  (case fast_term_ord tu of EQUAL => comments_ord tu | ord => ord);
    1.42 +
    1.43  end;
    1.44  
    1.45