1.1 --- a/src/Pure/Isar/element.ML	Mon Nov 05 17:48:17 2007 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Mon Nov 05 17:48:34 2007 +0100
     1.3 @@ -64,7 +64,6 @@
     1.4    val inst_term: typ Symtab.table * term Symtab.table -> term -> term
     1.5    val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
     1.6    val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
     1.7 -  val inst_morphism': theory -> typ Symtab.table * term Symtab.table -> typ Symtab.table * term Symtab.table -> morphism
     1.8    val satisfy_thm: witness list -> thm -> thm
     1.9    val satisfy_morphism: witness list -> morphism
    1.10    val satisfy_facts: witness list ->
    1.11 @@ -470,23 +469,15 @@
    1.12        fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)}
    1.13    end;
    1.14  
    1.15 -(* separate instantiation for theorems -- cannot have vars *)
    1.16 -fun inst_morphism' thy envs envs' =
    1.17 -  let val thy_ref = Theory.check_thy thy in
    1.18 -    Morphism.morphism
    1.19 -     {name = I, var = I,
    1.20 -      typ = instT_type (#1 envs),
    1.21 -      term = inst_term envs,
    1.22 -      fact = map (fn th => inst_thm (Theory.deref thy_ref) envs' th)}
    1.23 -  end;
    1.24 -
    1.25  
    1.26  (* satisfy hypotheses *)
    1.27  
    1.28  fun satisfy_thm witns thm = thm |> fold (fn hyp =>
    1.29      (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
    1.30        NONE => I
    1.31 -    | SOME (Witness (_, th)) => Drule.implies_intr_protected [hyp] #> Goal.comp_hhf th))
    1.32 +    | SOME (Witness (_, th)) => Drule.implies_intr_protected [hyp] #> 
    1.33 +          (fn thm' => Thm.implies_elim thm'
    1.34 +            (Thm.instantiate (Thm.match (cprop_of th, Drule.protect hyp)) th))))
    1.35    (#hyps (Thm.crep_thm thm));
    1.36  
    1.37  fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns);