src/HOL/Tools/inductive_realizer.ML
changeset 17959 8db36a108213
parent 17485 c39871c52977
child 18008 f193815cab2c
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Oct 21 18:14:37 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Oct 21 18:14:38 2005 +0200
     1.3 @@ -360,7 +360,7 @@
     1.4            (Extraction.realizes_of thy (vs @ Ps) r (prop_of induct)));
     1.5          val rews = map mk_meta_eq
     1.6            (fst_conv :: snd_conv :: get #rec_thms dt_info);
     1.7 -        val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
     1.8 +        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
     1.9            [if length rss = 1 then
    1.10               cut_facts_tac [hd prems] 1 THEN etac (#induct ind_info) 1
    1.11             else EVERY [rewrite_goals_tac (rews @ all_simps),
    1.12 @@ -410,7 +410,7 @@
    1.13          val rlz = strip_all (Logic.unvarify
    1.14            (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim)));
    1.15          val rews = map mk_meta_eq case_thms;
    1.16 -        val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
    1.17 +        val thm = OldGoals.simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems =>
    1.18            [cut_facts_tac [hd prems] 1,
    1.19             etac elimR 1,
    1.20             ALLGOALS (EVERY' [etac Pair_inject, asm_simp_tac HOL_basic_ss]),