# HG changeset patch
# User nipkow
# Date 800087932 -7200
# Node ID 7fca5aabcbb0f00f324848d6886451956eedd19e
# Parent  c2d51f10b9ee5f0d9a6a88dbbdcf477eb14b4a95
Modified translation for pattern abstraction.

diff -r c2d51f10b9ee -r 7fca5aabcbb0 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue May 09 22:10:48 1995 +0200
+++ b/src/ZF/ZF.thy	Wed May 10 08:38:52 1995 +0200
@@ -128,8 +128,8 @@
 
   "<x, y, z>"   == "<x, <y, z>>"
   "<x, y>"      == "Pair(x, y)"
-  "%<x,y,zs>.b"   => "split(%x <y,zs>.b)"
-  "%<x,y>.b"      => "split(%x y.b)"
+  "%<x,y,zs>.b"   == "split(%x <y,zs>.b)"
+  "%<x,y>.b"      == "split(%x y.b)"
 (* The <= direction fails if split has more than one argument because
    ast-matching fails.  Otherwise it would work fine *)
 
@@ -234,7 +234,7 @@
 ML
 
 (* Pattern-matching and 'Dependent' type operators *)
-
+(*
 local open Syntax
 
 fun pttrn s = const"@pttrn" $ s;
@@ -255,10 +255,11 @@
   in list_comb(const"_lambda" $ pttrn pats $ ft, args) end;
 
 in
-
+*)
 val print_translation = 
-  [("split", split_tr'),
+  [(*("split", split_tr'),*)
    ("Pi",    dependent_tr' ("@PROD", "op ->")),
    ("Sigma", dependent_tr' ("@SUM", "op *"))];
-
+(*
 end;
+*)