# HG changeset patch
# User wenzelm
# Date 1003766306 -7200
# Node ID a625de9ad62a3419e110dc9da8009b4324a6ca7e
# Parent  1a386a1e002c7c7d0b513d8ecfeb8579ac60bba3
quick_and_dirty_prove_goalw_cterm;

diff -r 1a386a1e002c -r a625de9ad62a src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon Oct 22 17:58:11 2001 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 22 17:58:26 2001 +0200
@@ -476,7 +476,7 @@
 
 fun prove_mono setT fp_fun monos thy =
  (message "  Proving monotonicity ...";
-  Goals.prove_goalw_cterm []      (*NO SkipProof.prove_goalw_cterm here!*)
+  Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
     (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
     (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
@@ -495,7 +495,7 @@
       | select_disj _ 1 = [rtac disjI1]
       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
 
-    val intrs = map (fn (i, intr) => SkipProof.prove_goalw_cterm thy rec_sets_defs
+    val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
       (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
        [(*insert prems and underlying sets*)
        cut_facts_tac prems 1,
@@ -524,7 +524,7 @@
     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
   in
     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
-      SkipProof.prove_goalw_cterm thy rec_sets_defs
+      quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
         (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
           [cut_facts_tac [hd prems] 1,
            dtac (unfold RS subst) 1,
@@ -652,14 +652,14 @@
     (* simplification rules for vimage and Collect *)
 
     val vimage_simps = if length cs < 2 then [] else
-      map (fn c => SkipProof.prove_goalw_cterm thy [] (Thm.cterm_of sign
+      map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign
         (HOLogic.mk_Trueprop (HOLogic.mk_eq
           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
              nth_elem (find_index_eq c cs, preds)))))
         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
 
-    val induct = SkipProof.prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
+    val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
         [rtac (impI RS allI) 1,
          DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
@@ -674,7 +674,7 @@
          EVERY (map (fn prem =>
            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
 
-    val lemma = SkipProof.prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
+    val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
         [cut_facts_tac prems 1,
          REPEAT (EVERY