# HG changeset patch
# User wenzelm
# Date 1369494814 -7200
# Node ID ceb31e1ded30f0726a8c8630b55dab225dcf865f
# Parent  28963df2dffbe739becd32af57fe7e0eccc59939
tuned;

diff -r 28963df2dffb -r ceb31e1ded30 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat May 25 17:08:43 2013 +0200
+++ b/src/HOL/Rat.thy	Sat May 25 17:13:34 2013 +0200
@@ -341,7 +341,7 @@
 proof -
   have "Fract a b = Fract (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?Fract)
     by (rule sym) (auto intro: normalize_eq)
-  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos) 
+  moreover have "0 < snd (normalize (a, b))" (is ?denom_pos)
     by (cases "normalize (a, b)") (rule normalize_denom_pos, simp)
   moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
     by (rule normalize_coprime) simp
@@ -1106,16 +1106,42 @@
   ord_rat_inst.less_eq_rat plus_rat_inst.plus_rat times_rat_inst.times_rat
   uminus_rat_inst.uminus_rat zero_rat_inst.zero_rat
 
-subsection{* Float syntax *}
+
+subsection {* Float syntax *}
 
 syntax "_Float" :: "float_const \<Rightarrow> 'a"    ("_")
 
-ML_file "Tools/float_syntax.ML"
-setup Float_Syntax.setup
+parse_translation {*
+  let
+    fun mk_number i =
+      let
+        fun mk 1 = Syntax.const @{const_syntax Num.One}
+          | mk i =
+              let val (q, r) = Integer.div_mod i 2
+              in HOLogic.mk_bit r $ (mk q) end;
+      in
+        if i = 0 then Syntax.const @{const_syntax Groups.zero}
+        else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
+        else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
+      end;
+
+    fun mk_frac str =
+      let
+        val {mant = i, exp = n} = Lexicon.read_float str;
+        val exp = Syntax.const @{const_syntax Power.power};
+        val ten = mk_number 10;
+        val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
+      in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
+
+    fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
+      | float_tr [t as Const (str, _)] = mk_frac str
+      | float_tr ts = raise TERM ("float_tr", ts);
+  in [(@{syntax_const "_Float"}, K float_tr)] end
+*}
 
 text{* Test: *}
 lemma "123.456 = -111.111 + 200 + 30 + 4 + 5/10 + 6/100 + (7/1000::rat)"
-by simp
+  by simp
 
 
 hide_const (open) normalize positive
diff -r 28963df2dffb -r ceb31e1ded30 src/HOL/Tools/float_syntax.ML
--- a/src/HOL/Tools/float_syntax.ML	Sat May 25 17:08:43 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-(*  Title:      HOL/Tools/float_syntax.ML
-    Author:     Tobias Nipkow, TU Muenchen
-
-Concrete syntax for floats.
-*)
-
-signature FLOAT_SYNTAX =
-sig
-  val setup: theory -> theory
-end;
-
-structure Float_Syntax: FLOAT_SYNTAX =
-struct
-
-(* parse translation *)
-
-local
-
-fun mk_number i =
-  let
-    fun mk 1 = Syntax.const @{const_syntax Num.One}
-      | mk i =
-          let val (q, r) = Integer.div_mod i 2
-          in HOLogic.mk_bit r $ (mk q) end;
-  in
-    if i = 0 then Syntax.const @{const_syntax Groups.zero}
-    else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i
-    else Syntax.const @{const_syntax Num.neg_numeral} $ mk (~i)
-  end;
-
-fun mk_frac str =
-  let
-    val {mant = i, exp = n} = Lexicon.read_float str;
-    val exp = Syntax.const @{const_syntax Power.power};
-    val ten = mk_number 10;
-    val exp10 = if n = 1 then ten else exp $ ten $ mk_number n;
-  in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end;
-
-in
-
-fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u
-  | float_tr [t as Const (str, _)] = mk_frac str
-  | float_tr ts = raise TERM ("float_tr", ts);
-
-end;
-
-
-(* theory setup *)
-
-val setup = Sign.parse_translation [(@{syntax_const "_Float"}, K float_tr)];
-
-end;