anchor.diff:  (* ------------------------------------------------------------------------- *)
   
   let new_definition tm =
  -  let avs,bod = strip_forall tm in
  -  let l,r = try dest_eq bod
  -    with Failure _ -> failwith "new_definition: Not an equation" in
  -  let lv,largs = strip_comb l in
  -  let rtm = try list_mk_abs(largs,r)
  -    with Failure _ -> failwith "new_definition: Non-variable in LHS pattern" in
  -  let def = mk_eq(lv,rtm) in
  -  let th1 = new_basic_definition def in
  -  let th2 = rev_itlist
  -    (fun tm th -> let ith = AP_THM th tm in
  -                  TRANS ith (BETA_CONV(rand(concl ith)))) largs th1 in
  -  let rvs = filter (not o C mem avs) largs in
  +  let avs,bod = strip_forall tm
  +  let l,r = 
  +    try dest_eq bod
  +    with Failure _ -> failwith "new_definition: Not an equation"
  +  let lv,largs = strip_comb l
  +  let rtm = 
  +    try list_mk_abs(largs,r)
  +    with Failure _ -> failwith "new_definition: Non-variable in LHS pattern"
  +  let def = mk_eq(lv,rtm)
  +  let th1 = new_basic_definition def
  +  let th2 = 
  +    rev_itlist (fun tm th -> 
  +      let ith = AP_THM th tm
  +      TRANS ith (BETA_CONV(rand(concl ith)))) largs th1
  +  let rvs = filter (not << C mem avs) largs in
     itlist GEN rvs (itlist GEN avs th2);;
  -
  -*)
  -
  
positive.code:         let th2 = GENL svs (DISCH ant (GENL pvs (UNDISCH th1))) in
          MP (DISCH tm th2) ith
      with Failure _ -> failwith "MATCH_MP: Not an implication" in
    let match_fun = PART_MATCH (fst o dest_imp) sth in
    fun th -> try MP (match_fun (concl th)) th
              with Failure _ -> failwith "MATCH_MP: No match";;
  
  
negative.code: 
  let (INSTANTIATE_ALL : instantiation->thm->thm) =
    fun ((_,tmin,tyin) as i) th ->
      if tmin = [] && tyin = [] then th else
      let hyps = hyp th in
      if hyps = [] then INSTANTIATE i th else
      let tyrel,tyiirel =
        if tyin = [] then [],hyps else
        let tvs = itlist (union << tyvars << snd) tyin [] in
        partition (fun tm -> let tvs' = type_vars_in_term tm in
                             not(intersect tvs tvs' = [])) hyps in
      let tmrel,tmirrel =
        if tmin = [] then [],tyiirel else
        let vs = itlist (union << frees << snd) tmin [] in
        partition (fun tm -> let vs' = frees tm in
                             not (intersect vs vs' = [])) tyiirel in
      let rhyps = union tyrel tmrel in
  