1.1 --- a/src/Provers/make_elim.ML	Fri Dec 30 16:56:59 2005 +0100
     1.2 +++ b/src/Provers/make_elim.ML	Fri Dec 30 16:57:00 2005 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Provers/make_elim.ML
     1.5 +(*  Title:      Provers/make_elim.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   2000  University of Cambridge
    1.10  
    1.11  Classical version of Tactic.make_elim
    1.12 @@ -15,34 +15,24 @@
    1.13  
    1.14  signature MAKE_ELIM_DATA =
    1.15  sig
    1.16 -  val classical	: thm		(* (~P ==> P) ==> P *)
    1.17 +  val cla_dist_concl: thm  (*"[| ~Z ==> PROP X; PROP Y ==> Z;  PROP X ==> PROP Y |] ==> Z"*)
    1.18  end;
    1.19  
    1.20  functor Make_Elim_Fun(Data: MAKE_ELIM_DATA)  =
    1.21  struct
    1.22  
    1.23 -local
    1.24 -    val cla_dist_concl = prove_goal (the_context ())
    1.25 -       "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_;  PROP X_ ==> PROP Y_ |] ==> Z_"
    1.26 -       (fn [premx,premz,premy] =>
    1.27 -	    ([(rtac Data.classical 1),
    1.28 -	      (etac (premx RS premy RS premz) 1)]))
    1.29 +fun make_elim rl =
    1.30 +  let
    1.31 +    fun compose_extra nsubgoal (tha,i,thb) =
    1.32 +      Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
    1.33 +    val revcut_rl' = Drule.incr_indexes rl revcut_rl
    1.34  
    1.35 -    fun compose_extra nsubgoal (tha,i,thb) =
    1.36 -	Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
    1.37 -
    1.38 -in
    1.39 -
    1.40 -fun make_elim rl =
    1.41 -    let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl
    1.42 -        fun making (i,rl) =
    1.43 -	    case compose_extra 2 (cla_dist_concl,i,rl) of
    1.44 -		[] => rl     (*terminates by clash of variables!*)
    1.45 -	      | rl'::_ => making (i+1,rl')
    1.46 +    fun making (i,rl) =
    1.47 +      case compose_extra 2 (Data.cla_dist_concl,i,rl) of
    1.48 +        [] => rl     (*terminates by clash of variables!*)
    1.49 +      | rl'::_ => making (i+1,rl')
    1.50      in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl')))  end
    1.51      handle (*in default, use the previous version, which never fails*)
    1.52 -	   THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
    1.53 +      THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
    1.54  
    1.55 -end
    1.56 - 
    1.57  end;