Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Morphism.thm_morphism;
authorwenzelm
Thu, 23 Nov 2006 20:33:36 +0100
changeset 21497 4d330a487586
parent 21496 a3ac0c55393f
child 21498 6382c3a1e7cf
Morphism.thm_morphism;
src/Pure/Isar/element.ML file | annotate | diff | comparison | revisions 
--- 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');
isabelle