always add pair rules and function update rules automatically (Boogie provides pairs and function update as built-in concepts and does not generate background axioms for them)

--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Wed Dec 15 10:12:44 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Wed Dec 15 10:12:48 2010 +0100
@@ -28,9 +28,13 @@
   let val unfold = Conv.rewrs_conv label_eqs
   in CONVERSION (Conv.top_sweep_conv (K unfold) ctxt) end
 
+val boogie_rules =
+  [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @
+  [@{thm fun_upd_same}, @{thm fun_upd_apply}]
+
 fun boogie_tac ctxt rules =
   unfold_labels_tac ctxt
-  THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ rules)
+  THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ boogie_rules @ rules)
 
 fun boogie_all_tac ctxt rules =
   PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules))