src/Pure/Proof/extraction.ML
changeset 27330 1af2598b5f7d
parent 27251 121991a4884d
child 27691 ce171cbd4b93
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Jun 23 20:00:58 2008 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Jun 23 23:45:39 2008 +0200
     1.3 @@ -128,10 +128,6 @@
     1.4  fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
     1.5  fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
     1.6  
     1.7 -fun forall_intr (t, prop) =
     1.8 -  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     1.9 -  in all T $ Abs (a, T, abstract_over (t, prop)) end;
    1.10 -
    1.11  fun forall_intr_prf (t, prf) =
    1.12    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    1.13    in Abst (a, SOME T, prf_abstract_over t prf) end;
    1.14 @@ -324,7 +320,7 @@
    1.15          (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
    1.16            (Const ("realizes", T --> propT --> propT) $
    1.17              (if T = nullT then t else list_comb (t, vars')) $ prop);
    1.18 -      val r = List.foldr forall_intr r' (map (get_var_type r') vars);
    1.19 +      val r = fold_rev Logic.all (map (get_var_type r') vars) r';
    1.20        val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
    1.21      in (name, (vs, (t, prf))) end
    1.22    end;