# HG changeset patch
# User wenzelm
# Date 964346542 -7200
# Node ID 612ee826a409c420a542d2ca9b84cc0a2fa536c8
# Parent  e769a6f8b333cefa9e79c597b6e91ecbf3b64e62
removed selector syntax -- improper tuples are broken beyond repair :-(

diff -r e769a6f8b333 -r 612ee826a409 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Sun Jul 23 12:01:39 2000 +0200
+++ b/src/HOL/Numeral.thy	Sun Jul 23 12:02:22 2000 +0200
@@ -2,16 +2,12 @@
     ID:         $Id$
     Author:     Larry Paulson and Markus Wenzel
 
-Generic numerals represented as twos-complement bit strings, and
-selector function as ones-complement unit strings.
+Generic numerals represented as twos-complement bit strings.
 *)
 
 theory Numeral = Datatype
 files "Tools/numeral_syntax.ML":
 
-
-(* numerals *)
-
 datatype
   bin = Pls
       | Min
@@ -28,73 +24,4 @@
 
 setup NumeralSyntax.setup
 
-
-(* selector functions *)
-
-(*Note that type constraints on selector functons are not handled
-  properly here*)
-
-syntax
-  "_selector" :: 'a
-  "_op_selector" :: "xnum => 'a"            ("op _" [0] 1000)
-
-translations
-  "(_Numeral i) x" => "_selector i x"
-
-parse_translation {*
-  let
-    val fstC = Syntax.const "fst";
-    val sndC = Syntax.const "snd";
-    fun ap_snd t = sndC $ t;
-    fun comp_snd t = Syntax.const "op o" $ t $ sndC;
-
-    fun selector_tr [Free (x, _), t] =
-          let val i = Syntax.read_xnum x in
-            if i = 0 orelse i = ~1 then t
-            else if i > 0 then fstC $ funpow (i - 1) ap_snd t
-            else funpow (~i - 1) ap_snd t
-          end
-      | selector_tr ts = raise TERM ("selector_tr", ts);
-
-    fun op_selector_tr [Free (x, _)] =
-          let val i = Syntax.read_xnum x in
-            if i = 0 orelse i = ~1 then Abs ("x", dummyT, Bound 0)
-            else if i > 0 then funpow (i - 1) comp_snd fstC
-            else funpow (~i - 2) comp_snd sndC
-          end
-      | op_selector_tr ts = raise TERM ("op_selector_tr", ts);
-  in [("_selector", selector_tr), ("_op_selector", op_selector_tr)] end
-*}
-
-print_translation {*
-  let
-    fun mk_xnum i =
-      Syntax.free ("#" ^ (if i < 0 then "-" else "") ^ (string_of_int (abs i)));
-
-
-    fun snds_tr' (i, Const ("snd", _) $ t) = snds_tr' (i + 1, t)
-      | snds_tr' x = x;
-
-    fun fst_tr' t = let val (i, t') = snds_tr' (0, t) in (i + 1, t') end;
-    fun snd_tr' t = let val (i, t') = snds_tr' (0, t) in (~ (i + 2), t') end;
-
-    fun selector_tr' f (t :: ts) =
-          let val (i, u) = f t in
-            if ~2 <= i andalso i <= 1 then raise Match
-            else Term.list_comb (mk_xnum i $ u, ts) end
-      | selector_tr' _ [] = raise Match;
-
-
-    fun o_snd_tr' i (Const ("op o", _) $ t $ Const ("snd", _)) = o_snd_tr' (i + 1) t
-      | o_snd_tr' i (Const ("fst", _)) = i + 1
-      | o_snd_tr' i (Const ("snd", _)) = ~ (i + 2)
-      | o_snd_tr' _ _ = raise Match;
-
-    fun comp_tr' (t :: u :: ts) =
-          Term.list_comb (Syntax.const "_op_selector" $
-            mk_xnum (o_snd_tr' 0 (Syntax.const "op o" $ t $ u)), ts)
-      | comp_tr' _ = raise Match;
-  in [("fst", selector_tr' fst_tr'), ("snd", selector_tr' snd_tr'), ("op o", comp_tr')] end
-*}
-
 end