src/HOL/Tools/datatype_realizer.ML
changeset 13708 a3a410782c95
parent 13656 58bb243dbafb
child 13725 12404b452034
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Nov 13 15:27:27 2002 +0100
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Nov 13 15:28:41 2002 +0100
     1.3 @@ -27,18 +27,6 @@
     1.4    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     1.5    in Abst (a, Some T, Proofterm.prf_abstract_over t prf) end;
     1.6  
     1.7 -fun prove_goal' sg p f =
     1.8 -  let
     1.9 -    val (As, B) = Logic.strip_horn p;
    1.10 -    val cAs = map (cterm_of sg) As;
    1.11 -    val asms = map (norm_hhf_rule o assume) cAs;
    1.12 -    fun check thm = if nprems_of thm > 0 then
    1.13 -      error "prove_goal': unsolved goals" else thm
    1.14 -  in
    1.15 -    standard (implies_intr_list cAs
    1.16 -      (check (Seq.hd (EVERY (f asms) (trivial (cterm_of sg B))))))
    1.17 -  end;
    1.18 -
    1.19  fun prf_of thm =
    1.20    let val {sign, prop, der = (_, prf), ...} = rep_thm thm
    1.21    in Reconstruct.reconstruct_proof sign prop prf end;
    1.22 @@ -129,7 +117,7 @@
    1.23      val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
    1.24        (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
    1.25  
    1.26 -    val thm = prove_goal' sg (Logic.list_implies (prems, concl))
    1.27 +    val thm = simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
    1.28        (fn prems =>
    1.29           [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
    1.30            rtac (cterm_instantiate inst induction) 1,