src/HOL/Tools/inductive_package.ML
changeset 17959 8db36a108213
parent 17485 c39871c52977
child 17985 d5d576b72371
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Oct 21 18:14:37 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Oct 21 18:14:38 2005 +0200
     1.3 @@ -472,7 +472,7 @@
     1.4  
     1.5  fun prove_mono setT fp_fun monos thy =
     1.6   (message "  Proving monotonicity ...";
     1.7 -  Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
     1.8 +  OldGoals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
     1.9      (Thm.cterm_of thy (HOLogic.mk_Trueprop
    1.10        (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
    1.11      (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
    1.12 @@ -491,7 +491,7 @@
    1.13        | select_disj _ 1 = [rtac disjI1]
    1.14        | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
    1.15  
    1.16 -    val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    1.17 +    val intrs = map (fn (i, intr) => OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    1.18        (Thm.cterm_of thy intr) (fn prems =>
    1.19         [(*insert prems and underlying sets*)
    1.20         cut_facts_tac prems 1,
    1.21 @@ -519,7 +519,7 @@
    1.22      val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
    1.23    in
    1.24      mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
    1.25 -      quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    1.26 +      OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
    1.27          (Thm.cterm_of thy t) (fn prems =>
    1.28            [cut_facts_tac [hd prems] 1,
    1.29             dtac (unfold RS subst) 1,
    1.30 @@ -648,7 +648,7 @@
    1.31      (* simplification rules for vimage and Collect *)
    1.32  
    1.33      val vimage_simps = if length cs < 2 then [] else
    1.34 -      map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
    1.35 +      map (fn c => OldGoals.quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
    1.36          (HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.37            (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
    1.38             HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
    1.39 @@ -661,7 +661,7 @@
    1.40  		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
    1.41  	    else ();
    1.42  
    1.43 -    val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
    1.44 +    val induct = OldGoals.quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
    1.45        (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
    1.46          [rtac (impI RS allI) 1,
    1.47           DETERM (etac raw_fp_induct 1),
    1.48 @@ -676,7 +676,7 @@
    1.49           EVERY (map (fn prem =>
    1.50     	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
    1.51  
    1.52 -    val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
    1.53 +    val lemma = OldGoals.quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
    1.54        (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
    1.55          [cut_facts_tac prems 1,
    1.56           REPEAT (EVERY