Abduction: remove simp_all from the Extend_Leaf strategy.

Some conjectures are easier to produce from a subgoal before
applying simplification to it.

For example, if smart_induct produces common-subgoals,
the conjecturing tool can apply common-subterm abstraction.

However, the simplifier may apply simplification rules that destroy
the property of having multiple occurrences of the same compoud sub-term.

Abduction/Abduction.thy

@@ -36,8 +36,8 @@ strategy Extend_Leaf =
   Alts [
     Clarsimp,
     Thens [
-      Smart_Induct,
-      User< simp_all>
+      Smart_Induct(*,
+      User< simp_all>*)
     ]
   ]
 

Abduction/All_Top_Down_Conjecturing.ML

@@ -31,23 +31,6 @@ in
   has_dupulicates: bool
 end;
 
-(* Prod31 for example needs this congruence(?).
-fun eq_over_same_func (ctxt:Proof.context) (trm:term) =
-  let
-    val trm_wo_Trueprop = Isabelle_Utils.remove_Trueprop trm;
-    val trm_w_prnt  = Unique_Node.trm_to_trm_w_prnt ctxt trm_wo_Trueprop;
-    val utrm_w_prnt = Unique_Node.trm_w_prnt_to_utrm_w_prnt trm_w_prnt;
-    val result = case utrm_w_prnt of
-        Unique_Node.UA_Prnt (Unique_Node.UC_Prnt ("HOL.eq", _, "HOL.eq"),
-          [Unique_Node.UA_Prnt (func1, _, _),
-           Unique_Node.UA_Prnt (func2, _, _)], _) => func1 = func2
-      | _ => false
-  in
-    result
-  end;
-*)
-
-
 fun template_conjectures (ctxt:Proof.context) (trm:term): (string * term) list =
   let
     val (_, relevant_binary_funcs, relevant_unary_funcs) = TBC_Utils.get_relevant_constants ctxt trm;