# HG changeset patch
# User wenzelm
# Date 1135958220 -3600
# Node ID 5cb04f20f46329e5afbc3253308d65a96bcb9f7e
# Parent  ce1ae48c320f57b91c3c9ce2278b81a765ddb52b
require cla_dist_concl, avoid assumptions about concrete syntax;

diff -r ce1ae48c320f -r 5cb04f20f463 src/Provers/make_elim.ML
--- a/src/Provers/make_elim.ML	Fri Dec 30 16:56:59 2005 +0100
+++ b/src/Provers/make_elim.ML	Fri Dec 30 16:57:00 2005 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	Provers/make_elim.ML
+(*  Title:      Provers/make_elim.ML
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   2000  University of Cambridge
 
 Classical version of Tactic.make_elim
@@ -15,34 +15,24 @@
 
 signature MAKE_ELIM_DATA =
 sig
-  val classical	: thm		(* (~P ==> P) ==> P *)
+  val cla_dist_concl: thm  (*"[| ~Z ==> PROP X; PROP Y ==> Z;  PROP X ==> PROP Y |] ==> Z"*)
 end;
 
 functor Make_Elim_Fun(Data: MAKE_ELIM_DATA)  =
 struct
 
-local
-    val cla_dist_concl = prove_goal (the_context ())
-       "[| ~Z_ ==> PROP X_; PROP Y_ ==> Z_;  PROP X_ ==> PROP Y_ |] ==> Z_"
-       (fn [premx,premz,premy] =>
-	    ([(rtac Data.classical 1),
-	      (etac (premx RS premy RS premz) 1)]))
-
+fun make_elim rl =
+  let
     fun compose_extra nsubgoal (tha,i,thb) =
-	Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
-
-in
+      Seq.list_of (bicompose false (false,tha,nsubgoal) i thb)
+    val revcut_rl' = Drule.incr_indexes rl revcut_rl
 
-fun make_elim rl =
-    let val revcut_rl' = incr_indexes_wrt [] [] [] [rl] revcut_rl
-        fun making (i,rl) =
-	    case compose_extra 2 (cla_dist_concl,i,rl) of
-		[] => rl     (*terminates by clash of variables!*)
-	      | rl'::_ => making (i+1,rl')
+    fun making (i,rl) =
+      case compose_extra 2 (Data.cla_dist_concl,i,rl) of
+        [] => rl     (*terminates by clash of variables!*)
+      | rl'::_ => making (i+1,rl')
     in  making (2, hd (compose_extra 1 (rl, 1, revcut_rl')))  end
     handle (*in default, use the previous version, which never fails*)
-	   THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
+      THM _ => Tactic.make_elim rl | Empty => Tactic.make_elim rl;
 
-end
- 
 end;