turned bicompose_no_flatten into compose_no_flatten, without elimination;
authorwenzelm
Fri Dec 23 15:16:52 2005 +0100 (2005-12-23)
changeset 18501915105af2e80
parent 18500 8b1a4e8ed199
child 18502 24efc1587f9d
turned bicompose_no_flatten into compose_no_flatten, without elimination;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Fri Dec 23 15:16:49 2005 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Dec 23 15:16:52 2005 +0100
     1.3 @@ -124,7 +124,7 @@
     1.4    val rotate_rule: int -> int -> thm -> thm
     1.5    val permute_prems: int -> int -> thm -> thm
     1.6    val rename_params_rule: string list * int -> thm -> thm
     1.7 -  val bicompose_no_flatten: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
     1.8 +  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
     1.9    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
    1.10    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
    1.11    val invoke_oracle: theory -> xstring -> theory * Object.T -> thm
    1.12 @@ -1456,11 +1456,11 @@
    1.13   end;
    1.14  end;
    1.15  
    1.16 -fun bicompose0 flatten match arg i state =
    1.17 -    bicompose_aux flatten match (state, dest_state(state,i), false) arg;
    1.18 +fun compose_no_flatten match (orule, nsubgoal) i state =
    1.19 +  bicompose_aux false match (state, dest_state (state, i), false) (false, orule, nsubgoal);
    1.20  
    1.21 -val bicompose_no_flatten = bicompose0 false;
    1.22 -val bicompose = bicompose0 true;
    1.23 +fun bicompose match arg i state =
    1.24 +  bicompose_aux true match (state, dest_state (state,i), false) arg;
    1.25  
    1.26  (*Quick test whether rule is resolvable with the subgoal with hyps Hs
    1.27    and conclusion B.  If eres_flg then checks 1st premise of rule also*)