putting proof in the right context; adding if rewriting; tuned

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Jul 21 09:46:36 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Jul 21 18:11:51 2010 +0200
@@ -114,7 +114,8 @@
     end
   else
     case (fst (strip_comb atom)) of
-      (Const (@{const_name If}, _)) => let
+      (Const (@{const_name If}, _)) =>
+        let
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
           val atom' = MetaSimplifier.rewrite_term thy
             (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
@@ -193,9 +194,10 @@
     val ((_, intros), ctxt') = Variable.import true intros ctxt
     val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
       (flatten constname) (map prop_of intros) ([], thy)
+    val ctxt'' = ProofContext.transfer thy' ctxt'
     val tac = fn _ => Skip_Proof.cheat_tac thy'
-    val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
-      |> Variable.export ctxt' ctxt
+    val intros'' = map (fn t => Goal.prove ctxt'' [] [] t tac) intros'
+      |> Variable.export ctxt'' ctxt
   in
     (intros'', (local_defs, thy'))
   end
@@ -287,6 +289,9 @@
         else
           error ("unexpected specification for constant " ^ quote constname ^ ":\n"
             ^ commas (map (quote o Display.string_of_thm_global thy) specs))
+      val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
+      val intros = map (MetaSimplifier.rewrite_rule
+          [if_beta RS @{thm eq_reflection}]) intros
       val _ = print_specs options thy "normalized intros" intros
       (*val intros = maps (split_cases thy) intros*)
       val (intros', (local_defs, thy')) = flatten_intros constname intros thy