generalized procs for rewrite_proof: allow skeleton;
fulfill_norm_proof: always normalize result here, no re-normalization after filling;

--- a/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 16 21:56:32 2009 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Mon Nov 16 21:57:16 2009 +0100
@@ -7,7 +7,7 @@
 signature REWRITE_HOL_PROOF =
 sig
   val rews: (Proofterm.proof * Proofterm.proof) list
-  val elim_cong: typ list -> Proofterm.proof -> Proofterm.proof option
+  val elim_cong: typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
 end;
 
 structure RewriteHOLProof : REWRITE_HOL_PROOF =
@@ -309,17 +309,19 @@
 
 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
 
-fun elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
-  | elim_cong Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
+  | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
         (strip_cong [] (incr_pboundvars 1 0 prf))
-  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
+  | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 [] o
         apsnd (map (make_sym Ts))) (strip_cong [] prf1)
-  | elim_cong Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
+  | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
         apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
-  | elim_cong _ _ = NONE;
+  | elim_cong_aux _ _ = NONE;
+
+fun elim_cong Ts prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
 
 end;

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Mon Nov 16 21:56:32 2009 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Mon Nov 16 21:57:16 2009 +0100
@@ -6,8 +6,9 @@
 
 signature PROOF_REWRITE_RULES =
 sig
-  val rew : bool -> typ list -> Proofterm.proof -> Proofterm.proof option
-  val rprocs : bool -> (typ list -> Proofterm.proof -> Proofterm.proof option) list
+  val rew : bool -> typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option
+  val rprocs : bool ->
+    (typ list -> Proofterm.proof -> (Proofterm.proof * Proofterm.proof) option) list
   val rewrite_terms : (term -> term) -> Proofterm.proof -> Proofterm.proof
   val elim_defs : theory -> bool -> thm list -> Proofterm.proof -> Proofterm.proof
   val elim_vars : (typ -> term) -> Proofterm.proof -> Proofterm.proof
@@ -183,7 +184,7 @@
         end
 
       | rew' _ = NONE;
-  in rew' end;
+  in rew' #> Option.map (rpair no_skel) end;
 
 fun rprocs b = [rew b];
 val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));

--- a/src/Pure/proofterm.ML	Mon Nov 16 21:56:32 2009 +0100
+++ b/src/Pure/proofterm.ML	Mon Nov 16 21:57:16 2009 +0100
@@ -109,18 +109,20 @@
   val axm_proof: string -> term -> proof
   val oracle_proof: string -> term -> oracle * proof
   val promise_proof: theory -> serial -> term -> proof
-  val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
+  val fulfill_norm_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> term list -> term ->
     (serial * proof_body future) list -> proof_body -> pthm * proof
   val get_name: term list -> term -> proof -> string
 
   (** rewriting on proof terms **)
   val add_prf_rrule: proof * proof -> theory -> theory
-  val add_prf_rproc: (typ list -> proof -> proof option) -> theory -> theory
+  val add_prf_rproc: (typ list -> proof -> (proof * proof) option) -> theory -> theory
+  val no_skel: proof
+  val normal_skel: proof
   val rewrite_proof: theory -> (proof * proof) list *
-    (typ list -> proof -> proof option) list -> proof -> proof
+    (typ list -> proof -> (proof * proof) option) list -> proof -> proof
   val rewrite_proof_notypes: (proof * proof) list *
-    (typ list -> proof -> proof option) list -> proof -> proof
+    (typ list -> proof -> (proof * proof) option) list -> proof -> proof
   val rew_proof: theory -> proof -> proof
 end
 
@@ -1169,28 +1171,30 @@
 
 (**** rewriting on proof terms ****)
 
-val skel0 = PBound 0;
+val no_skel = PBound 0;
+val normal_skel = Hyp (Var ((Name.uu, 0), propT));
 
 fun rewrite_prf tymatch (rules, procs) prf =
   let
-    fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, skel0)
-      | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, skel0)
-      | rew Ts prf = (case get_first (fn r => r Ts prf) procs of
-          SOME prf' => SOME (prf', skel0)
-        | NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
-            (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
-               handle PMatch => NONE) (filter (could_unify prf o fst) rules));
+    fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel)
+      | rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel)
+      | rew Ts prf =
+          (case get_first (fn r => r Ts prf) procs of
+            NONE => get_first (fn (prf1, prf2) => SOME (prf_subst
+              (match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2)
+                 handle PMatch => NONE) (filter (could_unify prf o fst) rules)
+          | some => some);
 
     fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) =
           if prf_loose_Pbvar1 prf' 0 then rew Ts prf
           else
             let val prf'' = incr_pboundvars (~1) 0 prf'
-            in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
+            in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
       | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
           if prf_loose_bvar1 prf' 0 then rew Ts prf
           else
             let val prf'' = incr_pboundvars 0 (~1) prf'
-            in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
+            in SOME (the_default (prf'', no_skel) (rew Ts prf'')) end
       | rew0 Ts prf = rew Ts prf;
 
     fun rew1 _ (Hyp (Var _)) _ = NONE
@@ -1205,20 +1209,20 @@
     and rew2 Ts skel (prf % SOME t) = (case prf of
             Abst (_, _, body) =>
               let val prf' = prf_subst_bounds [t] body
-              in SOME (the_default prf' (rew2 Ts skel0 prf')) end
-          | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf of
+              in SOME (the_default prf' (rew2 Ts no_skel prf')) end
+          | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf of
               SOME prf' => SOME (prf' % SOME t)
             | NONE => NONE))
       | rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
-          (rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf)
+          (rew1 Ts (case skel of skel' % _ => skel' | _ => no_skel) prf)
       | rew2 Ts skel (prf1 %% prf2) = (case prf1 of
             AbsP (_, _, body) =>
               let val prf' = prf_subst_pbounds [prf2] body
-              in SOME (the_default prf' (rew2 Ts skel0 prf')) end
+              in SOME (the_default prf' (rew2 Ts no_skel prf')) end
           | _ =>
             let val (skel1, skel2) = (case skel of
                 skel1 %% skel2 => (skel1, skel2)
-              | _ => (skel0, skel0))
+              | _ => (no_skel, no_skel))
             in case rew1 Ts skel1 prf1 of
                 SOME prf1' => (case rew1 Ts skel2 prf2 of
                     SOME prf2' => SOME (prf1' %% prf2')
@@ -1228,16 +1232,16 @@
                   | NONE => NONE)
             end)
       | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
-              (case skel of Abst (_, _, skel') => skel' | _ => skel0) prf of
+              (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
             SOME prf' => SOME (Abst (s, T, prf'))
           | NONE => NONE)
       | rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts
-              (case skel of AbsP (_, _, skel') => skel' | _ => skel0) prf of
+              (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
             SOME prf' => SOME (AbsP (s, t, prf'))
           | NONE => NONE)
       | rew2 _ _ _ = NONE;
 
-  in the_default prf (rew1 [] skel0 prf) end;
+  in the_default prf (rew1 [] no_skel prf) end;
 
 fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
   Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);
@@ -1249,7 +1253,9 @@
 
 structure ProofData = Theory_Data
 (
-  type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
+  type T =
+    (stamp * (proof * proof)) list *
+    (stamp * (typ list -> proof -> (proof * proof) option)) list;
 
   val empty = ([], []);
   val extend = I;
@@ -1277,27 +1283,26 @@
         | _ => false));
   in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
 
-fun fulfill_proof _ [] body0 = body0
-  | fulfill_proof thy ps body0 =
-      let
-        val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
-        val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
-        val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
-        val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
+fun fulfill_norm_proof thy ps body0 =
+  let
+    val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
+    val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
+    val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+    val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
 
-        fun fill (Promise (i, prop, Ts)) =
-            (case Inttab.lookup proofs i of
-              NONE => NONE
-            | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf))
-          | fill _ = NONE;
-        val (rules, procs) = get_data thy;
-        val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
-      in PBody {oracles = oracles, thms = thms, proof = proof} end;
+    fun fill (Promise (i, prop, Ts)) =
+          (case Inttab.lookup proofs i of
+            NONE => NONE
+          | SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf, normal_skel))
+      | fill _ = NONE;
+    val (rules, procs) = get_data thy;
+    val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
+  in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
 fun fulfill_proof_future _ [] body = Future.value body
   | fulfill_proof_future thy promises body =
       Future.fork_deps (map snd promises) (fn () =>
-        fulfill_proof thy (map (apsnd Future.join) promises) body);
+        fulfill_norm_proof thy (map (apsnd Future.join) promises) body);
 
 
 (***** theorems *****)

--- a/src/Pure/thm.ML	Mon Nov 16 21:56:32 2009 +0100
+++ b/src/Pure/thm.ML	Mon Nov 16 21:57:16 2009 +0100
@@ -540,7 +540,7 @@
 fun raw_body (Thm (Deriv {body, ...}, _)) = body;
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  Pt.fulfill_proof (Theory.deref thy_ref)
+  Pt.fulfill_norm_proof (Theory.deref thy_ref)
     (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
 and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));