Morphism.thm_morphism;
authorwenzelm
Thu Nov 23 20:33:36 2006 +0100 (2006-11-23)
changeset 214974d330a487586
parent 21496 a3ac0c55393f
child 21498 6382c3a1e7cf
Morphism.thm_morphism;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Thu Nov 23 20:33:34 2006 +0100
     1.2 +++ b/src/Pure/Isar/element.ML	Thu Nov 23 20:33:36 2006 +0100
     1.3 @@ -452,8 +452,7 @@
     1.4      | SOME (Witness (_, th)) => Drule.implies_intr_protected [hyp] #> Goal.comp_hhf th))
     1.5    (#hyps (Thm.crep_thm thm));
     1.6  
     1.7 -fun satisfy_morphism witns = Morphism.morphism
     1.8 -  {name = I, var = I, typ = I, term = I, thm = satisfy_thm witns};
     1.9 +fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns);
    1.10  
    1.11  fun satisfy_facts witns facts =
    1.12    morph_ctxt (satisfy_morphism witns) (Notes ("", facts)) |> (fn Notes (_, facts') => facts');