# HG changeset patch
# User wenzelm
# Date 1164310416 -3600
# Node ID 4d330a48758683ba02064dbded7506532c26bc1c
# Parent  a3ac0c55393fa222b023c6bd0eba7513803d3189
Morphism.thm_morphism;

diff -r a3ac0c55393f -r 4d330a487586 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Nov 23 20:33:34 2006 +0100
+++ b/src/Pure/Isar/element.ML	Thu Nov 23 20:33:36 2006 +0100
@@ -452,8 +452,7 @@
     | SOME (Witness (_, th)) => Drule.implies_intr_protected [hyp] #> Goal.comp_hhf th))
   (#hyps (Thm.crep_thm thm));
 
-fun satisfy_morphism witns = Morphism.morphism
-  {name = I, var = I, typ = I, term = I, thm = satisfy_thm witns};
+fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns);
 
 fun satisfy_facts witns facts =
   morph_ctxt (satisfy_morphism witns) (Notes ("", facts)) |> (fn Notes (_, facts') => facts');