src/HOL/Tools/datatype_realizer.ML
changeset 17959 8db36a108213
parent 17521 0f1c48de39f5
child 18358 0a733e11021a
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Fri Oct 21 18:14:37 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Fri Oct 21 18:14:38 2005 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4      val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
     1.5        (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
     1.6  
     1.7 -    val thm = simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
     1.8 +    val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl)))
     1.9        (fn prems =>
    1.10           [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
    1.11            rtac (cterm_instantiate inst induction) 1,
    1.12 @@ -190,7 +190,7 @@
    1.13      val y = Var (("y", 0), Type.varifyT T);
    1.14      val y' = Free ("y", T);
    1.15  
    1.16 -    val thm = prove_goalw_cterm [] (cert (Logic.list_implies (prems,
    1.17 +    val thm = OldGoals.prove_goalw_cterm [] (cert (Logic.list_implies (prems,
    1.18        HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
    1.19          list_comb (r, rs @ [y'])))))
    1.20        (fn prems =>