tuned satisfy_thm;
authorwenzelm
Mon Nov 05 23:17:03 2007 +0100 (2007-11-05)
changeset 2530219b1729f1bd4
parent 25301 24e027f55f45
child 25303 0699e20feabd
tuned satisfy_thm;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Mon Nov 05 23:17:02 2007 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Mon Nov 05 23:17:03 2007 +0100
     1.3 @@ -296,6 +296,12 @@
     1.4  fun conclude_witness (Witness (_, th)) =
     1.5    Goal.close_result (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
     1.6  
     1.7 +fun compose_witness (Witness (_, th)) r =
     1.8 +  let
     1.9 +    val th' = Goal.conclude th;
    1.10 +    val A = Thm.cprem_of r 1;
    1.11 +  in Thm.implies_elim r (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th') end;
    1.12 +
    1.13  val mark_witness = Logic.protect;
    1.14  
    1.15  fun make_witness t th = Witness (t, th);
    1.16 @@ -475,10 +481,7 @@
    1.17  fun satisfy_thm witns thm = thm |> fold (fn hyp =>
    1.18      (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
    1.19        NONE => I
    1.20 -    | SOME (Witness (_, th)) => Drule.implies_intr_protected [hyp] #> 
    1.21 -          (fn thm' => Thm.implies_elim thm'
    1.22 -            (Thm.instantiate (Thm.match (cprop_of th, Drule.protect hyp)) th))))
    1.23 -  (#hyps (Thm.crep_thm thm));
    1.24 +    | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
    1.25  
    1.26  fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns);
    1.27