1.1 --- a/src/Pure/Proof/proofchecker.ML	Sat Nov 15 21:31:30 2008 +0100
     1.2 +++ b/src/Pure/Proof/proofchecker.ML	Sat Nov 15 21:31:32 2008 +0100
     1.3 @@ -45,7 +45,7 @@
     1.4          Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
     1.5        end;
     1.6  
     1.7 -    fun thm_of _ _ (PThm (name, _, prop', SOME Ts)) =
     1.8 +    fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
     1.9            let
    1.10              val thm = Drule.implies_intr_hyps (lookup name);
    1.11              val {prop, ...} = rep_thm thm;

     2.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Nov 15 21:31:30 2008 +0100
     2.2 +++ b/src/Pure/Proof/reconstruct.ML	Sat Nov 15 21:31:32 2008 +0100
     2.3 @@ -220,7 +220,7 @@
     2.4                   add_cnstrt Ts (v $ t) (prf % SOME t) cnstrts env3 vTs'
     2.5                     (u, Const ("all", (T --> propT) --> propT) $ v)
     2.6                 end)
     2.7 -      | mk_cnstrts env _ _ vTs (prf as PThm (_, _, prop, opTs)) =
     2.8 +      | mk_cnstrts env _ _ vTs (prf as PThm (_, ((_, prop, opTs), _))) =
     2.9            mk_cnstrts_atom env vTs prop opTs prf
    2.10        | mk_cnstrts env _ _ vTs (prf as PAxm (_, prop, opTs)) =
    2.11            mk_cnstrts_atom env vTs prop opTs prf
    2.12 @@ -323,7 +323,7 @@
    2.13        Const ("==>", _) $ P $ Q => Q
    2.14      | _ => error "prop_of: ==> expected")
    2.15    | prop_of0 Hs (Hyp t) = t
    2.16 -  | prop_of0 Hs (PThm (_, _, prop, SOME Ts)) = prop_of_atom prop Ts
    2.17 +  | prop_of0 Hs (PThm (_, ((_, prop, SOME Ts), _))) = prop_of_atom prop Ts
    2.18    | prop_of0 Hs (PAxm (_, prop, SOME Ts)) = prop_of_atom prop Ts
    2.19    | prop_of0 Hs (Oracle (_, prop, SOME Ts)) = prop_of_atom prop Ts
    2.20    | prop_of0 _ _ = error "prop_of: partial proof object";
    2.21 @@ -350,7 +350,7 @@
    2.22        | expand maxidx prfs (prf % t) =
    2.23            let val (maxidx', prfs', prf') = expand maxidx prfs prf
    2.24            in (maxidx', prfs', prf' % t) end
    2.25 -      | expand maxidx prfs (prf as PThm (a, cprf, prop, SOME Ts)) =
    2.26 +      | expand maxidx prfs (prf as PThm (_, ((a, prop, SOME Ts), body))) =
    2.27            if not (exists
    2.28              (fn (b, NONE) => a = b
    2.29                | (b, SOME prop') => a = b andalso prop = prop') thms)
    2.30 @@ -365,7 +365,7 @@
    2.31                      val _ = message ("Reconstructing proof of " ^ a);
    2.32                      val _ = message (Syntax.string_of_term_global thy prop);
    2.33                      val prf' = forall_intr_vfs_prf prop
    2.34 -                      (reconstruct_proof thy prop cprf);
    2.35 +                      (reconstruct_proof thy prop (force_proof body));
    2.36                      val (maxidx', prfs', prf) = expand
    2.37                        (maxidx_proof prf' ~1) prfs prf'
    2.38                    in (maxidx' + maxidx + 1, inc (maxidx + 1) prf,