merge

--- a/src/HOL/Library/Extended_Real.thy	Wed Jul 20 16:14:49 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Jul 20 16:15:33 2011 +0200
@@ -75,6 +75,15 @@
     and MInfty_cases[simp]: "(case - \<infinity> of ereal r \<Rightarrow> f r | PInfty \<Rightarrow> y | MInfty \<Rightarrow> z) = z"
   by (simp_all add: infinity_ereal_def)
 
+declare
+  PInfty_eq_infinity[code_post]
+  MInfty_eq_minfinity[code_post]
+
+lemma [code_unfold]:
+  "\<infinity> = PInfty"
+  "-PInfty = MInfty"
+  by simp_all
+
 lemma inj_ereal[simp]: "inj_on ereal A"
   unfolding inj_on_def by auto
 
@@ -2540,4 +2549,14 @@
   "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
   by (metis sup_ereal_def sup_least)
 
+subsubsection {* Tests for code generator *}
+
+(* A small list of simple arithmetic expressions *)
+
+value [code] "- \<infinity> :: ereal"
+value [code] "\<bar>-\<infinity>\<bar> :: ereal"
+value [code] "4 + 5 / 4 - ereal 2 :: ereal"
+value [code] "ereal 3 < \<infinity>"
+value [code] "real (\<infinity>::ereal) = 0"
+
 end

--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 16:14:49 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Jul 20 16:15:33 2011 +0200
@@ -554,11 +554,9 @@
       ts2
       |> eta_expand ctxt1 is_fol funcs
       |> rpair ctxt1
-      |>> tap (map (tracing o PolyML.makestring))
       |-> Lambda_Lifting.lift_lambdas NONE is_binder
       |-> (fn (ts', defs) => fn ctxt' =>
           map mk_trigger defs @ ts'
-          |> tap (map (tracing o PolyML.makestring))
           |> intro_explicit_application ctxt' funcs 
           |> pair ctxt')