diff -r 829e684b02ef -r 49f602ae24e5 src/HOL/Real/float_syntax.ML
--- a/src/HOL/Real/float_syntax.ML	Fri Dec 05 11:26:07 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(*  ID:         $Id$
-    Authors:    Tobias Nipkow, TU Muenchen
-
-Concrete syntax for floats
-*)
-
-signature FLOAT_SYNTAX =
-sig
-  val setup: theory -> theory
-end;
-
-structure FloatSyntax: FLOAT_SYNTAX =
-struct
-
-(* parse translation *)
-
-local
-
-fun mk_number i =
-  let
-    fun mk 0 = Syntax.const @{const_name Int.Pls}
-      | mk ~1 =  Syntax.const @{const_name Int.Min}
-      | mk i = let val (q, r) = Integer.div_mod i 2
-               in HOLogic.mk_bit r $ (mk q) end;
-  in Syntax.const @{const_name Int.number_of} $ mk i end;
-
-fun mk_frac str =
-  let
-    val {mant=i, exp = n} = Syntax.read_float str;
-    val exp = Syntax.const @{const_name "Power.power"};
-    val ten = mk_number 10;
-    val exp10 = if n=1 then ten else exp $ ten $ (mk_number n);
-  in (Syntax.const @{const_name "divide"}) $ (mk_number i) $ exp10 end
-in
-
-fun float_tr (*"_Float"*) [t as Const (str, _)] = mk_frac str
-  | float_tr (*"_Float"*) ts = raise TERM ("float_tr", ts);
-
-end;
-
-
-(* theory setup *)
-
-val setup =
-  Sign.add_trfuns ([], [("_Float", float_tr)], [], []);
-
-end;