--- a/Nominal/Tacs.thy	Tue May 25 00:24:41 2010 +0100
+++ b/Nominal/Tacs.thy	Wed May 26 15:34:54 2010 +0200
@@ -17,44 +17,7 @@
 end
 *}
 
-ML {*
-fun mk_conjl props =
-  fold (fn a => fn b =>
-    if a = @{term True} then b else
-    if b = @{term True} then a else
-    HOLogic.mk_conj (a, b)) (rev props) @{term True};
-*}
 
-ML {*
-val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
-*}
-
-(* Given function for buildng a goal for an input, prepares a
-   one common goals for all the inputs and proves it by induction
-   together *)
-ML {*
-fun prove_by_induct tys build_goal ind utac inputs ctxt =
-let
-  val names = Datatype_Prop.make_tnames tys;
-  val (names', ctxt') = Variable.variant_fixes names ctxt;
-  val frees = map Free (names' ~~ tys);
-  val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt';
-  val gls = flat gls_lists;
-  fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls;
-  val trm_gl_lists = map trm_gls_map frees;
-  val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists
-  val trm_gls = map mk_conjl trm_gl_lists;
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls);
-  fun tac {context,...} = (
-    InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind]
-    THEN_ALL_NEW split_conj_tac THEN_ALL_NEW utac) 1
-  val th_loc = Goal.prove ctxt'' [] [] gl tac
-  val ths_loc = HOLogic.conj_elims th_loc
-  val ths = Variable.export ctxt'' ctxt ths_loc
-in
-  filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
-end
-*}
 
 ML {*
 fun prove_by_rel_induct alphas build_goal ind utac inputs ctxt =
@@ -83,41 +46,6 @@
   filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths
 end
 *}
-(* Code for transforming an inductive relation to a function *)
-ML {*
-fun rel_inj_tac dist_inj intrs elims =
-  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
-  (rtac @{thm iffI} THEN' RANGE [
-     (eresolve_tac elims THEN_ALL_NEW
-       asm_full_simp_tac (HOL_ss addsimps dist_inj)
-     ),
-     asm_full_simp_tac (HOL_ss addsimps intrs)])
-*}
-
-ML {*
-fun build_rel_inj_gl thm =
-  let
-    val prop = prop_of thm;
-    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
-    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
-    fun list_conj l = foldr1 HOLogic.mk_conj l;
-  in
-    if hyps = [] then concl
-    else HOLogic.mk_eq (concl, list_conj hyps)
-  end;
-*}
-
-ML {*
-fun build_rel_inj intrs dist_inj elims ctxt =
-let
-  val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
-  val gls = map (HOLogic.mk_Trueprop o build_rel_inj_gl) thms_imp;
-  fun tac _ = rel_inj_tac dist_inj intrs elims 1;
-  val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
-in
-  Variable.export ctxt' ctxt thms
-end
-*}
 
 ML {*
 fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm