in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;

     in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;

 fun instT_morphism thy env =

 fun instT_morphism thy env =

   let val thy_ref = Theory.check_thy thy in

   let val thy_ref = Theory.check_thy thy in

     Morphism.morphism

     Morphism.morphism

       typ = [instT_type env],

       typ = [instT_type env],

       term = [instT_term env],

       term = [instT_term env],

       fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]}

       fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]}

   end;

   end;