1.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 01 11:18:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Jun 01 11:30:57 2010 +0200
     1.3 @@ -22,10 +22,6 @@
     1.4      in map (fn ks => i::ks) is @ is end
     1.5    else [[]];
     1.6  
     1.7 -fun forall_intr_prf (t, prf) =
     1.8 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     1.9 -  in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
    1.10 -
    1.11  fun prf_of thm =
    1.12    Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
    1.13  
    1.14 @@ -130,12 +126,12 @@
    1.15  
    1.16      val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
    1.17      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    1.18 -    val ivs1 = map Var (filter_out (fn (_, T) =>  (* FIXME set (!??) *)
    1.19 -      member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs);
    1.20 +    val ivs1 = map Var (filter_out (fn (_, T) =>
    1.21 +      @{type_name bool} = tname_of (body_type T)) ivs);
    1.22      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
    1.23  
    1.24      val prf =
    1.25 -      List.foldr forall_intr_prf
    1.26 +      Extraction.abs_corr_shyps thy' induct vs ivs2
    1.27          (fold_rev (fn (f, p) => fn prf =>
    1.28            (case head_of (strip_abs_body f) of
    1.29               Free (s, T) =>
    1.30 @@ -145,7 +141,7 @@
    1.31                 end
    1.32            | _ => AbsP ("H", SOME p, prf)))
    1.33              (rec_fns ~~ prems_of thm)
    1.34 -            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))) ivs2;
    1.35 +            (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
    1.36  
    1.37      val r' =
    1.38        if null is then r
    1.39 @@ -198,18 +194,21 @@
    1.40        ||> Sign.restore_naming thy;
    1.41  
    1.42      val P = Var (("P", 0), rT' --> HOLogic.boolT);
    1.43 -    val prf = forall_intr_prf (y, forall_intr_prf (P,
    1.44 -      fold_rev (fn (p, r) => fn prf =>
    1.45 -          forall_intr_prf (Logic.varify_global r, AbsP ("H", SOME (Logic.varify_global p), prf)))
    1.46 +    val prf = Extraction.abs_corr_shyps thy' exhaust ["P"] [y, P]
    1.47 +      (fold_rev (fn (p, r) => fn prf =>
    1.48 +          Proofterm.forall_intr_proof' (Logic.varify_global r)
    1.49 +            (AbsP ("H", SOME (Logic.varify_global p), prf)))
    1.50          (prems ~~ rs)
    1.51 -        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0)))));
    1.52 +        (Proofterm.proof_combP (prf_of thm', map PBound (length prems - 1 downto 0))));
    1.53 +    val prf' = Extraction.abs_corr_shyps thy' exhaust []
    1.54 +      (map Var (Term.add_vars (prop_of exhaust) [])) (prf_of exhaust);
    1.55      val r' = Logic.varify_global (Abs ("y", T,
    1.56        list_abs (map dest_Free rs, list_comb (r,
    1.57          map Bound ((length rs - 1 downto 0) @ [length rs])))));
    1.58  
    1.59    in Extraction.add_realizers_i
    1.60      [(exh_name, (["P"], r', prf)),
    1.61 -     (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy'
    1.62 +     (exh_name, ([], Extraction.nullt, prf'))] thy'
    1.63    end;
    1.64  
    1.65  fun add_dt_realizers config names thy =