# HG changeset patch
# User nipkow
# Date 1306962484 -7200
# Node ID faba4800b00bc2d60fdc34a964723806b055757f
# Parent  9ed5d8ad8fa048565682eea48bbc7d2ba6a18bac# Parent  631dd866b2847aff408d59ec75a43feb545905cb
merged

diff -r 631dd866b284 -r faba4800b00b src/HOL/Library/Extended_Reals.thy
--- a/src/HOL/Library/Extended_Reals.thy	Wed Jun 01 22:47:26 2011 +0200
+++ b/src/HOL/Library/Extended_Reals.thy	Wed Jun 01 23:08:04 2011 +0200
@@ -74,10 +74,10 @@
   fixes a :: extreal shows "- (- a) = a"
   by (cases a) simp_all
 
-lemma MInfty_eq[simp]:
+lemma MInfty_eq[simp, code_post]:
   "MInfty = - \<infinity>" by simp
 
-declare uminus_extreal.simps(2)[simp del]
+declare uminus_extreal.simps(2)[code_inline, simp del]
 
 lemma extreal_cases[case_names real PInf MInf, cases type: extreal]:
   assumes "\<And>r. x = extreal r \<Longrightarrow> P"
diff -r 631dd866b284 -r faba4800b00b src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 22:47:26 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 23:08:04 2011 +0200
@@ -1056,9 +1056,7 @@
              else
                accum
            else
-             let
-               val ary = length args
-             in
+             let val ary = length args in
                (ho_var_Ts,
                 case Symtab.lookup sym_tab s of
                   SOME {pred_sym, min_ary, max_ary, types} =>
@@ -1099,18 +1097,18 @@
   fact_lift (formula_fold NONE
                           (K (add_combterm_syms_to_table ctxt explicit_apply)))
 
-val default_sym_table_entries : (string * sym_info) list =
-  [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
-   (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}),
-   (make_fixed_const predicator_name,
-    {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @
+val default_sym_tab_entries : (string * sym_info) list =
+  (make_fixed_const predicator_name,
+   {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
   ([tptp_false, tptp_true]
-   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []}))
+   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
+  ([tptp_equal, tptp_old_equal]
+   |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
 
 fun sym_table_for_facts ctxt explicit_apply facts =
   Symtab.empty
-  |> fold Symtab.default default_sym_table_entries
   |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
+  |> fold Symtab.update default_sym_tab_entries
 
 fun min_arity_of sym_tab s =
   case Symtab.lookup sym_tab s of