Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_term.ML
changeset 1000 1893316b9ef8
parent 999 64874975f087
child 1065 3664eafcad09 
--- a/Quot/quotient_term.ML	Mon Feb 01 09:47:46 2010 +0100
+++ b/Quot/quotient_term.ML	Mon Feb 01 10:00:03 2010 +0100
@@ -446,14 +446,14 @@
          if ty = ty' then subtrm
          else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
        end
-  | (Const (@{const_name "Babs"}, T) $ r $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
+  | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
        let
          val subtrm = regularize_trm ctxt (t, t')
          val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
        in
-         if r <> needres
-         then term_mismatch "regularize (Babs)" ctxt r needres
-         else mk_babs $ r $ subtrm
+         if resrel <> needres
+         then term_mismatch "regularize (Babs)" ctxt resrel needres
+         else mk_babs $ resrel $ subtrm
        end
 
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
@@ -491,7 +491,6 @@
          else mk_ball $ (mk_resp $ resrel) $ subtrm
        end
 
-
   | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
      Const (@{const_name "Ex"}, ty') $ t') =>
        let
@@ -556,16 +555,16 @@
            end
        end 
 
-  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, Abs(v1', ty', s1))),
-     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , Abs(v2', _  , s2)))) =>
-       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, Abs(v1', ty', regularize_trm ctxt (s1, s2)))
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
+       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
 
-  | (((t1 as Const (@{const_name "split"}, _)) $ Abs(v1, ty, s1)),
-     ((t2 as Const (@{const_name "split"}, _)) $ Abs(v2, _ , s2))) =>
-       (regularize_trm ctxt (t1, t2)) $ Abs(v1, ty, regularize_trm ctxt (s1, s2))
+  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
+     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
+       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
 
   | (t1 $ t2, t1' $ t2') =>
-       (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2'))
+       regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
 
   | (Bound i, Bound i') =>
        if i = i' then rtrm
nominal2